jmlspecs-interest — Discussions of the JML language and semantics; post problems as support requests

[Jmlspecs-interest] Open call for software submissions Science of Computer Programming - Software Track

[Huisman, M. (UT-EEMCS) <m.h...@ut...>]

Open call for software submissions
Science of Computer Programming - Software Track

The Science of Computer Programming journal is dedicated to the distribution of research results in the areas of software systems development, use and maintenance, including the software aspects of hardware design. In addition to regular journal papers, the Software Track of Science of Computer Programming makes it possible to publish your software in the form of Original Software Publications (OSP). The Software Track is targeting software whose underlying research fits within the scope of Science of Computer Programming, such as for example formal methods or empirical software engineering.

The Software Track enables dissemination of existing and useful software in the areas of programming (languages) and software development. Research on programming and software development may involve the creation of (huge) software systems to perform all kinds of experiments related to programming (languages) and software development. An OSP comprises in the first place a tool, in the second place a short (typically, around six pages) description of the tool, formatted as a regular SCP submission. The source code (or a link to it) and documentary material (such as user manuals) must be part of the submission. Supplementary material such as test cases, design documents and more are welcome, too, when they can help readers and users get going with the tool and the ideas behind it. The contributions should be innovative. The software must adhere to a recognized legal license, such as the Open Source Initiative approved licenses.

Importantly, the software will be a full publication that is able to capture your software updates as and once they are released. To fully acknowledge the author's/developer's software work your software will be fully citable as an Original Software Publication, archived and indexed and available as a complete online "body of work" for other researchers and practitioners to discover.

When submitting to the SCP Software Track, your software will be reviewed by subject experts on:
- The originality, novelty, and significance of the contribution.
- The quality, completeness, and readability of the source code.
- The quality of the documentation (both for users and developers).
- The reproducibility of the empirical results (results shown in tables and figures can be reproduced by reviewer and users).
- The accessibility of the software (is it easy to configure and use).
- The quality of the accompanying manuscript (is it clear what the software does?).

Detailed submission instructions can be found under the journal-specific information on the website of SCP:
https://www.sciencedirect.com/journal/science-of-computer-programming/publish/guide-for-authors#toc-59

The accompanying article can be published as gold open access of OA agreements between Elsevier and one of the authors' institutions agreement or in case authors pay the Article Publishing Charges (APCs) for short articles (see https://www.elsevier.com/about/policies-and-standards/pricing for full details).

If you have any questions, you can contact the associate editor-in-chief of the SCP Software Track via sci...@gm...<mailto:sci...@gm...>.

[Jmlspecs-interest] Deadline extension TAP 2024 (Tests and Proofs 2024), Milan, Italy: new submission deadline June 14

[Huisman, M. (UT-EEMCS) <m.h...@ut...>]

*Many good reasons to submit your paper to TAP*



TAP submission deadline has been extended to June 14 (with optional abstract submission deadline June 12), see https://tapconference.github.io/2024/ for all information.



We are excited to announce that we

  *   Rosemary Monahan<https://www.maynoothuniversity.ie/faculty-science-engineering/our-people/rosemary-monahan> (Maynooth University, Ireland)
  *   Rüdiger Ehlers<https://www.isse.tu-clausthal.de/ueber-uns/team-neu/professoren-und-dozenten/prof-dr-ruediger-ehlers> (TU Clausthal, Germany)

will be this year’s invited speakers for TAP.

TAP will be colocated with a number of long standing and reknown formal methods conferences in the week of September 9th in Milan, Italy. Namely:

- FM: https://www.fm24.polimi.it/
- FMICS: https://fmics.inria.fr/2024/
- PPDP: https://ppdp2024.github.io/
- LOPSTR: https://lopstr.github.io/2024/
- FACS: https://facs-conference.github.io/2024/

There will also be an industry day and workshops. The list of workshops is: FMxSL, PAVeTrust, CPA, Overture, and FMTea

We look forward to your submissions!

Falk Howar and Marieke Huisman
PC chairs TAP 2024





TAP 2024 - Call for Papers



***********************************************************************************************************************

The 18th International Conference on Tests and Proofs (TAP 2024)

https://tapconference.github.io/2024/



co-located within FM 2024 (Formal Methods 2024)

https://www.fm24.polimi.it/



***********************************************************************************************************************


Aim and Scope
-------------
TAP 2024 is the 18th International Conference on Tests and Proofs. TAP promotes research in verification and formal methods that targets the
interplay of static and dynamic analysis techniques with the ultimate goal of improving software and system dependability.

Research in verification has seen an increase in heterogeneous techniques and a synergy between the traditionally distinct areas of dynamic and static analysis. There is growing awareness that dynamic techniques such as testing and static techniques such as proving are complementary rather than mutually exclusive. Notable examples that provide evidence for the potential of a combination of static and dynamic analysis are counterexample generation based on symbolic execution, the integration of SAT/SMT-solving in model checking, or the combination of predicate abstraction with exhaustive enumeration. The verification of systems based on machine learning spurs novel combinations of dynamic and static analyses, e.g., property verification of surrogate models that are generated through testing.

TAP’s scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Topics of interest center around the combination of static techniques such as proving and dynamic techniques such as testing.

Papers are solicited on, but not limited to, the following topics:

- Verification and analysis techniques combining proofs and tests,
- Static analysis of programs with the aid of dynamic techniques,
- Deductive techniques supporting the automated generation of test vectors and oracles,
- Deductive techniques supporting (novel) definitions of coverage criteria,
- Specification inference by deductive or dynamic methods,
- Testing and runtime analysis of formal specifications,
- Search-based techniques for proving and testing,
- Testing and Verification of systems based on machine learning,
- Verification of verification tools and environments,
- Applications of test and proof techniques in new domains,
- Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, …), and
- Case studies, tool and framework descriptions, and experience reports

Authors are encouraged (but not required) to make the relevant artifacts available to the reviewers (and whenever possible publicly). Artifacts can be provided at submission time or after notification of acceptance and will go through a lightweight  reviewing process, handing out availability badges.


Important Dates
---------------

Abstract submission (optional):   June 12, 2024
Paper submission:      June 14, 2024
Paper notification:    July 5, 2024
Artifact submission:   July 7, 2024
Artifact notification: July 14, 2024
Camera-ready version:  July 19, 2024

Conference: September 9 – 10, 2024


Submission Instructions
-------------

TAP 2024 accepts papers of two kinds:

- Regular papers: full submissions describing
  - original research results,
  - tools, and
  - case studies
of up to 16 pages. For tools and case studies, the tool, framework, or case study described in a tool paper should be available for public use.
 - Short papers: submissions describing preliminary findings, proofs of concepts, and exploratory studies, of up to 6 pages.

All page limits exclude the references. Appendices may be included, but they will only be read by a reviewer at their discretion.

Regular and short papers must be original, unpublished, and not submitted for publication elsewhere.

Papers will undergo a thorough review process. The review process is single blind. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. The submissions will be reviewed and selected for publication based on the above-mentioned
criteria as well as suitability to the conference’s technical program. After notification, all artifacts of accepted papers will be reviewed
with respect to their availability, consistency with and replicability of results in the paper, completeness, documentation, and ease of use.
The papers will receive corresponding badges.

Accepted submissions will be published in Springer’s LNCS series. Papers have to adhere to Springer’s LNCS format and must be submitted in PDF
format at the EasyChair submission site:

https://easychair.org/my/conference?conf=tap24

[Jmlspecs-interest] Open Position: Malware Detection 2.0 with Control-Flow Fingerprinting

[Richard B. <bu...@cs...>]

# Malware Detection 2.0 with Control-Flow Fingerprinting 

Our group (Software Engineering Group, (Software Engineering Group, [Prof. Reiner Hähnle](https://www.informatik.tu-darmstadt.de/se/gruppenmitglieder/groupmembers_detailseite_30784.en.jsp), TU Darmstadt, Germany) is looking for a *PhD student* or *PostDoc* who is interested in working with us on a project in the intersection of **Formal Methods** and **IT Security**.

The project aims to detect malware based on a new, semantic approach called **Control-Flow Fingerprinting**. The idea is to compute a profile of a program's behavior by recording and classifying its logic decisions. The ambition is to be able to detect supply chain attacks targeting source code repositories as reported here:

 https://apiiro.com/blog/malicious-code-campaign-github-repo-confusion-attack/
 
### What we offer
We are an internationally leading research group in the areas of deductive program verification and formal analysis of distributed systems.

We offer an engaging atmosphere, interesting research topics and collaboration with excellent researchers. The project you will work on is a joint effort with Profs. Haya Schulmann and Michael Waidner, who are internationally leading experts in the field of IT security.

The project is financed by the **National Research Center for Applied Cybersecurity ATHENE**, which offers a stimulating and vibrant environment with numerous offers of collaboration, distinguished lectures, exchange with political decision makers, etc.

PhD students and PostDocs are employed on a time-limited contract (usually, 3 years, with possible extension up to two years to complete a PhD). The salary depends on the experience level and starts at around 4,200 EUR per month (before taxes). Employment in Germany includes health insurance.  

### What you should offer
You have a keen interest in and excellent knowledge about formal
methods (preferably: logic-based approaches). The project will involve tool building, so we expect very good software engineering skills. If you apply with the aim to achieve a PhD, your masters thesis was research-oriented, preferably having resulted in a first publication. In any case, it is necessary to provide evidence of your talent to perform scientific research.

### How to apply?
Your application (in German or English) must consist of a *single* PDF document and include: (i) a motivation letter that states why you are interested in the position and why you are qualified, (ii) a CV, (iii) certificates and transcripts with detailed grades for M.Sc., B.Sc., and high school diploma, (iv) masters/bachelor/PhD thesis, as applicable. If you are applying as a PostDoc, please include the evidence of the successful completion of the Ph.D. (certificate). Instead of including a thesis you may also provide a download link.

Send your application via email to: 

 Prof. Reiner Hähnle, <se...@cs...> 

stating reference number **127** (this is **essential**).
 
-- 
Richard Bubel, FG Software Engineering, TU Darmstadt

[Jmlspecs-interest] Snd CfP: TAP 2024 (Tests and Proofs 2024), Milan, Italy

[Huisman, M. (UT-EEMCS) <m.h...@ut...>]

This is just a quick reminder that the deadline for submissions are May 8th (abstracts) and May 15th (papers):  https://tapconference.github.io/2024/

TAP will be colocated with a number of long standing and reknown formal methods conferences in the week of September 9th in Milan, Italy. Namely:

- FM: https://www.fm24.polimi.it/
- FMICS: https://fmics.inria.fr/2024/
- PPDP: https://ppdp2024.github.io/
- LOPSTR: https://lopstr.github.io/2024/
- FACS: https://facs-conference.github.io/2024/

There will also be an industry day and workshops. The list of workshops is: FMxSL, PAVeTrust, CPA, Overture, and FMTea





TAP 2024 - Call for Papers



***********************************************************************************************************************

The 18th International Conference on Tests and Proofs (TAP 2024)

https://tapconference.github.io/2024/



co-located within FM 2024 (Formal Methods 2024)

https://www.fm24.polimi.it/



***********************************************************************************************************************


Aim and Scope
-------------
TAP 2024 is the 18th International Conference on Tests and Proofs. TAP promotes research in verification and formal methods that targets the
interplay of static and dynamic analysis techniques with the ultimate goal of improving software and system dependability.

Research in verification has seen an increase in heterogeneous techniques and a synergy between the traditionally distinct areas of dynamic and static analysis. There is growing awareness that dynamic techniques such as testing and static techniques such as proving are complementary rather than mutually exclusive. Notable examples that provide evidence for the potential of a combination of static and dynamic analysis are counterexample generation based on symbolic execution, the integration of SAT/SMT-solving in model checking, or the combination of predicate abstraction with exhaustive enumeration. The verification of systems based on machine learning spurs novel combinations of dynamic and static analyses, e.g., property verification of surrogate models that are generated through testing.

TAP’s scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Topics of interest center around the combination of static techniques such as proving and dynamic techniques such as testing.

Papers are solicited on, but not limited to, the following topics:

- Verification and analysis techniques combining proofs and tests,
- Static analysis of programs with the aid of dynamic techniques,
- Deductive techniques supporting the automated generation of test vectors and oracles,
- Deductive techniques supporting (novel) definitions of coverage criteria,
- Specification inference by deductive or dynamic methods,
- Testing and runtime analysis of formal specifications,
- Search-based techniques for proving and testing,
- Testing and Verification of systems based on machine learning,
- Verification of verification tools and environments,
- Applications of test and proof techniques in new domains,
- Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, …), and
- Case studies, tool and framework descriptions, and experience reports

Authors are encouraged (but not required) to make the relevant artifacts available to the reviewers (and whenever possible publicly). Artifacts can be provided at submission time or after notification of acceptance and will go through a lightweight  reviewing process, handing out availability badges.


Important Dates
---------------

Abstract submission:   05/08/2024
Paper submission:      05/15/2024
Paper notification:    06/26/2024
Artifact submission:   07/03/2024
Artifact notification: 07/14/2024
Camera-ready version:  07/17/2024

Conference: 09/09/2024-09/10/2024


Submission Instructions
-------------

TAP 2024 accepts papers of two kinds:

- Regular papers: full submissions describing
  - original research results,
  - tools, and
  - case studies
of up to 16 pages. For tools and case studies, the tool, framework, or case study described in a tool paper should be available for public use.

- Short papers: submissions describing preliminary findings, proofs of concepts, and exploratory studies, of up to 6 pages.

All page limits exclude the references. Appendices may be included, but they will only be read by a reviewer at their discretion.

Regular and short papers must be original, unpublished, and not submitted for publication elsewhere.

Papers will undergo a thorough review process. The review process is single blind. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. The submissions will be reviewed and selected for publication based on the above-mentioned
criteria as well as suitability to the conference’s technical program. After notification, all artifacts of accepted papers will be reviewed
with respect to their availability, consistency with and replicability of results in the paper, completeness, documentation, and ease of use.
The papers will receive corresponding badges.

Accepted submissions will be published in Springer’s LNCS series. Papers have to adhere to Springer’s LNCS format and must be submitted in PDF
format at the EasyChair submission site:

https://easychair.org/my/conference?conf=tap24

[Jmlspecs-interest] Call for Papers: TAP 2024 (Tests and Proofs 2024), Milan, Italy

[Huisman, M. (UT-EEMCS) <m.h...@ut...>]

TAP 2024 - Call for Papers





***********************************************************************************************************************

The 18th International Conference on Tests and Proofs (TAP 2024)

https://tapconference.github.io/2024/



co-located within FM 2024 (Formal Methods 2024)

https://www.fm24.polimi.it/



***********************************************************************************************************************


Aim and Scope
-------------
TAP 2024 is the 18th International Conference on Tests and Proofs. TAP promotes research in verification and formal methods that targets the
interplay of static and dynamic analysis techniques with the ultimate goal of improving software and system dependability.

Research in verification has seen an increase in heterogeneous techniques and a synergy between the traditionally distinct areas of dynamic and static analysis. There is growing awareness that dynamic techniques such as testing and static techniques such as proving are complementary rather than mutually exclusive. Notable examples that provide evidence for the potential of a combination of static and dynamic analysis are counterexample generation based on symbolic execution, the integration of SAT/SMT-solving in model checking, or the combination of predicate abstraction with exhaustive enumeration. The verification of systems based on machine learning spurs novel combinations of dynamic and static analyses, e.g., property verification of surrogate models that are generated through testing.

TAP’s scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Topics of interest center around the combination of static techniques such as proving and dynamic techniques such as testing.

Papers are solicited on, but not limited to, the following topics:

- Verification and analysis techniques combining proofs and tests,
- Static analysis of programs with the aid of dynamic techniques,
- Deductive techniques supporting the automated generation of test vectors and oracles,
- Deductive techniques supporting (novel) definitions of coverage criteria,
- Specification inference by deductive or dynamic methods,
- Testing and runtime analysis of formal specifications,
- Search-based techniques for proving and testing,
- Testing and Verification of systems based on machine learning,
- Verification of verification tools and environments,
- Applications of test and proof techniques in new domains,
- Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, …), and
- Case studies, tool and framework descriptions, and experience reports

Authors are encouraged (but not required) to make the relevant artifacts available to the reviewers (and whenever possible publicly). Artifacts can be provided at submission time or after notification of acceptance and will go through a lightweight  reviewing process, handing out availability badges.


Important Dates
---------------

Abstract submission:   05/08/2024
Paper submission:      05/15/2024
Paper notification:    06/26/2024
Artifact submission:   07/03/2024
Artifact notification: 07/14/2024
Camera-ready version:  07/17/2024

Conference: 09/09/2024-09/10/2024


Submission Instructions
-------------

TAP 2024 accepts papers of two kinds:

- Regular papers: full submissions describing
  - original research results,
  - tools, and
  - case studies
of up to 16 pages. For tools and case studies, the tool, framework, or case study described in a tool paper should be available for public use.

- Short papers: submissions describing preliminary findings, proofs of concepts, and exploratory studies, of up to 6 pages.

All page limits exclude the references. Appendices may be included, but they will only be read by a reviewer at their discretion.

Regular and short papers must be original, unpublished, and not submitted for publication elsewhere.

Papers will undergo a thorough review process. The review process is single blind. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. The submissions will be reviewed and selected for publication based on the above-mentioned
criteria as well as suitability to the conference’s technical program. After notification, all artifacts of accepted papers will be reviewed
with respect to their availability, consistency with and replicability of results in the paper, completeness, documentation, and ease of use.
The papers will receive corresponding badges.

Accepted submissions will be published in Springer’s LNCS series. Papers have to adhere to Springer’s LNCS format and must be submitted in PDF
format at the EasyChair submission site:

https://easychair.org/my/conference?conf=tap24

[Jmlspecs-interest] PhD position on Program Analysis for LLVM-IR and all its source languages @ University of Twente, Netherlands

[Huisman, M. (UT-EEMCS) <m.h...@ut...>]

PhD position on Program Analysis for LLVM-IR and all its source languages
University of Twente, Netherlands
To apply, visit: https://utwentecareers.nl/en/vacancies/1320/phd-position-on-program-analysis-for-llvm-ir-and-all-its-source-languages/

* The project *

Formal verification can play an important role to ensure that software is free of errors. To enable formal verification for many different programming languages, we will develop a deductive verifier for an intermediate language, and then build deductive verifiers for many different source languages on top of this.

With the omnipresence of software, our lives and income depend crucially on the quality of software: software failures can cause planes to crash, emergency service to be unreachable, and companies to lose millions of dollars (because of missed business opportunities, but also due to reputation damage). Therefore, software developers are urgently looking for techniques that can help them to improve the quality of their software. Formal verification techniques that allow one to prove that software will never reach an erroneous state can play an essential role in this. However, to use this in an industrial setting, we need to make sure that the verification technology can be used in combination with the newest programming language technology. Deductive program verification is a formal verification technique that works directly at the code level, and non-trivial case studies have shown its potential. However, for its widespread use, we need tool support for many different programming languages, which requires a large amount of engineering.

Therefore, in this project, you will be working on a different approach. Rather than building a deductive program verifier for each programming language, you will develop deductive program verification technology for the widely-used intermediate representation language LLVM-IR. You can use deductive verification for any programming language that compiles into the LLVM-IR format.

In addition, you will define a generic specification format to write the program specifications, which is then automatically compiled into a specified LLVM-IR program, and which can be verified. Finally, you will also develop techniques to give feedback on failed verification attempts at the level of the source program, rather than asking the developer to study the generated LLVM-IR code. Throughout the project, you will evaluate the verification technology on various industrial case studies, including applications that use multiple programming languages, that are all targeting the LLVM-IR format.

You will work on this project in close collaboration with the members of the VerCors team, who are working on the VerCors program verifier (see utwente.nl/vercors/).

* Your profile *

- You are an enthusiastic and highly motivated researcher.
- You have, or will shortly, acquire a master's degree in the field of Computer Science, or comparable.
- You have a demonstrable interest in formal specification and verification and an affinity with tool development.
- You have a creative mentality and excellent analytical and communication skills.
- You have a good team spirit and like to work in an interdisciplinary and internationally oriented environment.
- You are proficient in English.

* Our offer *

- As a PhD candidate at UT, you will be appointed to a full-time position for four years, with a qualifier in the first year, within a very stimulating and exciting scientific environment;
- You will be a member of the Formal Methods and Tools research group, a strong research group on formal verification, with an open and welcoming atmosphere;
- The University offers a dynamic ecosystem with enthusiastic colleagues;
- Your salary and associated conditions are in accordance with the collective labour agreement for Dutch universities (CAO-NU);
- You will receive a gross monthly salary ranging from € 2.541,- (first year) to € 3.247,- (fourth year);
- There are excellent benefits including a holiday allowance of 8% of the gross annual salary, an end-of-year bonus of 8.3%, and a solid pension scheme;
- The flexibility to work (partially) from home;
- A minimum of 232 leave hours in case of full-time employment based on a formal workweek of 38 hours. Full-time employment in practice means 40 hours a week, therefore resulting in 96 extra leave hours on an annual basis.
- Free access to sports facilities on campus
- A family-friendly institution that offers parental leave (both paid and unpaid);
- You will have a training programme as part of the Twente Graduate School where you and your supervisors will determine a plan for a suitable education and supervision;
- We encourage a high degree of responsibility and independence while collaborating with close colleagues, researchers and other staff.

* Information and application *

Are you interested in this position? Please send your application via the 'Apply now' button below before August 31, 2023, and include:

- A cover letter (maximum 2 pages A4), emphasizing your motivation to apply for this specific position.
- A Curriculum Vitae, including a list of all courses attended and grades obtained, and, if applicable, a list of publications and references.
- The names of 2 or 3 people who can be contacted for additional information about you.

For more information regarding this position, you are welcome to contact prof.dr. Marieke Huisman, m.h...@ut...<mailto:m.h...@ut...>

Interviews are scheduled in September.

To apply, visit https://utwentecareers.nl/en/vacancies/1320/phd-position-on-program-analysis-for-llvm-ir-and-all-its-source-languages/

[Jmlspecs-interest] JML - watching and participating in ongoing work

[David C. <dav...@gm...>]

Hi,

David Cok, Mattias Ulbrich, and I have settled on using github's JavaModelingLanguage/RefMan repository for JML language design discussions, as we are trying to put out a revised reference manual.  We are posting language design issue notes on the issues tracker for that repository, so please visit

  https://github.com/JavaModelingLanguage/RefMan/issues <https://github.com/JavaModelingLanguage/RefMan/issues>

to see the current issues and discussions and watch the project (by clicking on the "Watch" button) at

  https://github.com/JavaModelingLanguage/RefMan <https://github.com/JavaModelingLanguage/RefMan>

to stay up to date.  We value your contributions and thoughts.

Furthermore, we expect to discontinue use of the jmlspecs-* set of mailing lists and the sourceforge project for JML.

Both the JML and OpenJML projects are active on GitHub - JML as above and OpenJML at GitHub.com/openjml <http://github.com/openjml> and www.openjml.org <http://www.openjml.org/>

       Regards,

       Gary T. Leavens
       329 L3Harris Center
       Computer Science, University of Central Florida
       4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
       http://www.cs.ucf.edu/~leavens <http://www.cs.ucf.edu/~leavens> phone: +1-407-823-4758
       Le...@uc... <mailto:Le...@uc...>

[Jmlspecs-interest] PhD Position available in the KeY project

[Richard B. <bu...@cs...>]

Dear all,

we are currently looking for PhD students in the context of the research project “KeY – A deductive software analysis tool for the research community” funded by the DFG (German Science Foundation).

The next step is to improve KeY’s usability and performance to a degree that puts it in reach of the average software developer. This includes the modernization and modularisation of the code base, the creation of an active research and user community around KeY to achieve sustainable usage and development of the KeY software platform.

== What we offer ==

* Fully funded PhD position at German E13 scale for up to 5 years
* To make a real difference in rendering verification technology widely usable, long after your PhD is finished
* Working together with world leaders at the cutting edge of Deductive Verification at TU Darmstadt and KIT (Karlsruhe), Germany
* A dedicated, friendly, and supportive team, good social atmosphere, pleasant offices, coffee machine
* Opportunity to take soft skill courses, teaching certificates, etc.

Interested? You find more information and how to apply at
   https://www.key-project.org/help-to-push-software-verification-to-the-next-level/
    
Best Regards,
Richard 

—  
Richard Bubel, FG Software Engineering, TU Darmstadt

[Jmlspecs-interest] assistant/associate professor in formal methods and programming, at University of Twente

[cok <co...@fr...>]

> 
> From: "m.h...@ut... <mailto:m.h...@ut...>" <m.h...@ut... <mailto:m.h...@ut...>>
> Subject: assistant/associate professor in formal methods and programming, at University of Twente
> Date: June 30, 2021 at 10:15:26 AM EDT
> To: "m.h...@ut... <mailto:m.h...@ut...>" <m.h...@ut... <mailto:m.h...@ut...>>
> 
> 
> The Formal Methods and Tools (FMT) group of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) of the University of Twente is looking for an Assistant/Associate Professor in the area of formal methods and programming.
>  
> You will teach in - and contribute to the degree programmes of Computer Science and Creative Technology, and you will participate in the teaching program of specialized courses related to Software Technology in Computer Science. In particular, the candidate is expected to contribute to programming education in the first and second year of Creative Technology, as well teaching a course on Principles of Programming, Processes and Patterns Programming and supervising Software Technology students during their Industrial Software Engineering Project.
>  
> The FMT Group: 
>  
> The mission of FMT is to develop mathematical methods, high-performance data structures and algorithms, and suitable programming languages for the design of reliable software- and data-intensive control systems. We focus on modelling, synthesis, analysis, prediction, and maintenance of their functional, structural and quantitative aspects. We aim to understand a complex systems’ safety, reliability, performance, energy usage and the risks and costs associated to its architecture, design, operation, and maintenance.
>  
> Our mission builds on extensive experience in concurrency theory, static analysis, theorem proving, language design, model checking and term/graph rewriting.
> More information about the group: https://www.utwente.nl/en/eemcs/fmt/ <https://www.utwente.nl/en/eemcs/fmt/>
>  
> FMT embraces scholarship in learning and teaching. We are proudly involved in education at all levels: In undergraduate and graduate university curricula, primary and secondary schools, teacher education, extracurricular programs, and post-graduate teaching. We use the classroom setting in our research, co-publish with students, and do active research on educational research.
>  
> FMT has is an open and welcoming group. We value social interaction and transparency, and we value the input of all members of the group.
>  
> Your profile
>  
> You have a strong interest and shown ability to collaborate in an academic, multidisciplinary environment. A successful candidate will also demonstrate her or his intrinsic motivation and strong abilities for teaching at the bachelor and master level, and to various groups of students. You have excellent communication skills, allowing efficient interaction with colleagues.
>  
> Furthermore, we encourage you to apply if:
> You have a PhD degree in Computer Science or a related discipline;
> You are capable of strengthening the FMT group;
> You have strong abilities for high-quality research and teaching in a multidisciplinary context;
> You are effective in acquiring external funding;
> You are fluent in English. Knowledge of, or willingness to learn Dutch is an advantage;
> You have a University Teaching Qualification (Dutch: BKO) or equivalent, or are willing to acquire one within three years.
>  
> Our offer
> We offer a fulltime structural position, starting with a temporary appointment with the prospect of a permanent position after a positive evaluation;
> Our terms of employment are in accordance with the Dutch Collective Labor Agreement for Universities (CAO) and include a holiday allowance of 8% of the gross annual salary and a year-end bonus of 8.3 %;
> Depending on your relevant background and experience, the gross monthly salary on a full-time basis ranges from € 3.746,-  to € 6.940,- per month;
> A minimum of 29 leave days in case of full-time employment based on a formal workweek of 38 hours. A fulltime employment in practice means 40 hours a week, therefore resulting in 96 extra leave hours on an annual basis;
> Furthermore, we offer excellent professional and personal development programs;
> Finally, you will work in a lively, inspiring and dynamic working environment in an organization focusing on internationalization, where you will have a high degree of responsibility and independence.
>  
> Information and application
>  
> Are you interested in joining our team? Please submit your application before the 14th of July 2021, via https://www.utwente.nl/en/organisation/careers/!/50/ <https://www.utwente.nl/en/organisation/careers/!/50/>, including:
> A curriculum vitae (including, list of publications, research and teaching statement)
> A cover letter in which you describe your motivation and qualifications for the position.
>  
> You are welcome to contact prof.dr. M. Huisman via m.h...@ut... <mailto:m.h...@ut...>, for any questions you might have.
>  
> About the organization
>  
> The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.
>  
> As an employer, the EEMCS Faculty offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With our Faculty, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customizable conditions.
>  
> University of Twente (UT)
>  
> University of Twente (UT) has entered the new decade with an ambitious, new vision, mission and strategy. As ‘the ultimate people-first university of technology' we are rapidly expanding on our High Tech Human Touch philosophy and the unique role it affords us in society. Everything we do is aimed at maximum impact on people, society and connections through the sustainable utilisation of science and technology. We want to contribute to the development of a fair, digital and sustainable society through our open, inclusive and entrepreneurial attitude. This attitude permeates everything we do and is present in every one of UT's departments and faculties. Building on our rich legacy in merging technical and social sciences, we focus on five distinguishing research domains: Improving healthcare by personalised technologies; Creating intelligent manufacturing systems; Shaping our world with smart materials; Engineering our digital society; and Engineering for a resilient world.
>  
> As an employer, University of Twente offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With us, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customisable conditions.
>  
> 
> 
> 
> From: jml...@li... <mailto:jml...@li...>
> Subject: confirm f81bceadd198607af3583f4b35448682376c913a
> Date: June 30, 2021 at 10:16:18 AM EDT
> 
> 
> If you reply to this message, keeping the Subject: header intact,
> Mailman will discard the held message.  Do this if the message is
> spam.  If you reply to this message and include an Approved: header
> with the list password in it, the message will be approved for posting
> to the list.  The Approved: header can also appear in the first line
> of the body of the reply.

[Jmlspecs-interest] assistant/associate professor in formal methods and programming, at University of Twente

[<m.h...@ut...>]

The Formal Methods and Tools (FMT) group of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) of the University of Twente is looking for an Assistant/Associate Professor in the area of formal methods and programming.

You will teach in - and contribute to the degree programmes of Computer Science and Creative Technology, and you will participate in the teaching program of specialized courses related to Software Technology in Computer Science. In particular, the candidate is expected to contribute to programming education in the first and second year of Creative Technology, as well teaching a course on Principles of Programming, Processes and Patterns Programming and supervising Software Technology students during their Industrial Software Engineering Project.

The FMT Group:

The mission of FMT is to develop mathematical methods, high-performance data structures and algorithms, and suitable programming languages for the design of reliable software- and data-intensive control systems. We focus on modelling, synthesis, analysis, prediction, and maintenance of their functional, structural and quantitative aspects. We aim to understand a complex systems’ safety, reliability, performance, energy usage and the risks and costs associated to its architecture, design, operation, and maintenance.

Our mission builds on extensive experience in concurrency theory, static analysis, theorem proving, language design, model checking and term/graph rewriting.
More information about the group: https://www.utwente.nl/en/eemcs/fmt/

FMT embraces scholarship in learning and teaching. We are proudly involved in education at all levels: In undergraduate and graduate university curricula, primary and secondary schools, teacher education, extracurricular programs, and post-graduate teaching. We use the classroom setting in our research, co-publish with students, and do active research on educational research.

FMT has is an open and welcoming group. We value social interaction and transparency, and we value the input of all members of the group.

Your profile

You have a strong interest and shown ability to collaborate in an academic, multidisciplinary environment. A successful candidate will also demonstrate her or his intrinsic motivation and strong abilities for teaching at the bachelor and master level, and to various groups of students. You have excellent communication skills, allowing efficient interaction with colleagues.

Furthermore, we encourage you to apply if:

  *   You have a PhD degree in Computer Science or a related discipline;
  *   You are capable of strengthening the FMT group;
  *   You have strong abilities for high-quality research and teaching in a multidisciplinary context;
  *   You are effective in acquiring external funding;
  *   You are fluent in English. Knowledge of, or willingness to learn Dutch is an advantage;
  *   You have a University Teaching Qualification (Dutch: BKO) or equivalent, or are willing to acquire one within three years.

Our offer

  *   We offer a fulltime structural position, starting with a temporary appointment with the prospect of a permanent position after a positive evaluation;
  *   Our terms of employment are in accordance with the Dutch Collective Labor Agreement for Universities (CAO) and include a holiday allowance of 8% of the gross annual salary and a year-end bonus of 8.3 %;
  *   Depending on your relevant background and experience, the gross monthly salary on a full-time basis ranges from € 3.746,-  to € 6.940,- per month;
  *   A minimum of 29 leave days in case of full-time employment based on a formal workweek of 38 hours. A fulltime employment in practice means 40 hours a week, therefore resulting in 96 extra leave hours on an annual basis;
  *   Furthermore, we offer excellent professional and personal development programs;
  *   Finally, you will work in a lively, inspiring and dynamic working environment in an organization focusing on internationalization, where you will have a high degree of responsibility and independence.

Information and application

Are you interested in joining our team? Please submit your application before the 14th of July 2021, via https://www.utwente.nl/en/organisation/careers/!/50/, including:

  *   A curriculum vitae (including, list of publications, research and teaching statement)
  *   A cover letter in which you describe your motivation and qualifications for the position.

You are welcome to contact prof.dr. M. Huisman via m.h...@ut..., for any questions you might have.

About the organization

The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.

As an employer, the EEMCS Faculty offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With our Faculty, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customizable conditions.

University of Twente (UT)

University of Twente (UT) has entered the new decade with an ambitious, new vision, mission and strategy. As ‘the ultimate people-first university of technology' we are rapidly expanding on our High Tech Human Touch philosophy and the unique role it affords us in society. Everything we do is aimed at maximum impact on people, society and connections through the sustainable utilisation of science and technology. We want to contribute to the development of a fair, digital and sustainable society through our open, inclusive and entrepreneurial attitude. This attitude permeates everything we do and is present in every one of UT's departments and faculties. Building on our rich legacy in merging technical and social sciences, we focus on five distinguishing research domains: Improving healthcare by personalised technologies; Creating intelligent manufacturing systems; Shaping our world with smart materials; Engineering our digital society; and Engineering for a resilient world.

As an employer, University of Twente offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With us, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customisable conditions.

[Jmlspecs-interest] PhD position on Embedded Systems Verification at University of Twente, Netherlands

[<m.h...@ut...>]

We are looking for a PhD candidate for a 4-year project on Formal Methods for Embedded Systems, as part of SAVES (ScAlable Verification of industrial Embedded control Systems), a collaboration with the University of Münster (WWU Münster). You will be working on the SAVES project, carried out in collaboration with prof. dr. Paula Herber (University of Twente / WWU Münster).

The overall goal of SAVES is to investigate methods and tools to establish correctness of embedded systems. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. At the same time, we see that in the area of deductive program verification, powerful techniques and tools have been developed to reason about software with unbounded parameters, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems.

The PhD candidate hired at the University of Twente will be supervised by Marieke Huisman and Paula Herber and will work on extensions of the methods and tools developed in the FMT group for embedded systems, in close collaboration with the Embedded Systems group in Münster.

For further information about the group, see https://www.utwente.nl/en/eemcs/fmt/. For further information about the project, see https://www.utwente.nl/en/eemcs/fmt/research/projects/saves/.

YOUR PROFILE


  *   You have a MSc degree in Computer Science (or equivalent);
  *   You have a thorough theoretical background and a demonstrable interest in embedded or cyber-physical systems, and ideally some prior experience with embedded systems design, formal methods, and/or interactive theorem provers;
  *   You are an enthusiastic student, skilled in exact and abstract thinking;
  *   You are proficient in English on an academic level.

OUR OFFER

The terms of employment are in accordance with the Dutch Collective Labour Agreement for Universities (CAO) and include:


  *   A fulltime PhD position for four years, with a qualifier in the first year;
  *   Full status as an employee at the UT, including pension and health care benefits;
  *   The salary will range from € 2.395 (1st year) to € 3.061,- (4th year) per month, plus a holiday allowance of 8% and a year-end bonus of 8.3%;
  *   A solid pension scheme;
  *   Excellent facilities for professional and personal development;
  *   A green and lively campus, with lots of sports facilities and other activities.

INFORMATION AND APPLICATION

Are you interested in this position? Please send your application via https://www.utwente.nl/en/organisation/careers/!/2021-425/phd-position-on-embedded-systems- before 5th of July and include:


  *   A cover letter (explaining your specific interest and qualifications);
  *   A detailed Curriculum Vitae;
  *   A list of all courses + marks and a short description of your MSc thesis;
  *   References (contact information) of two scientific staff members.


The deadline of application is July 5, 2021 or until the position is filled. Starting date of the position is as soon as possible, or to be discussed.

For further information, you can contact Prof.dr.ir. Paula Herber: https://www.uni-muenster.de/EmbSys/team/herber/ or Prof.dr. Marieke Huisman: https://wwwhome.ewi.utwente.nl/~marieke/

DEPARTMENT
In the Formal Methods and Tools (FMT) research group, formal techniques and tools are developed and used as a means to support the development of software. Our central goal is to increase the reliability of the software that we rely on, as individuals and as society. We primarily target complex concurrent ICT systems, embedded in a technological context or in a distributed environment.

The FMT group is part of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente. The FMT group also participates in the Digital Systems Institute (DSI).

Our institute was ranked first at the most recent research national assessment.

ORGANIZATION
The faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) uses mathematics, electronics and computer technology to contribute to the development of Information and Communication Technology (ICT). With ICT present in almost every device and product we use nowadays, we embrace our role as contributors to a broad range of societal activities and as pioneers of tomorrow's digital society. As part of a people-first tech university that aims to shape society, individuals and connections, our faculty works together intensively with industrial partners and researchers in the Netherlands and abroad, and conducts extensive research for external commissioning parties and funders. Our research has a high profile both in the Netherlands and internationally. It has been accommodated in three multidisciplinary UT research institutes: Mesa+ Institute, TechMed Centre and Digital Society Institute.

As an employer, the EEMCS Faculty offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With our Faculty, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customizable conditions.

UNIVERSITY OF TWENTE (UT)
University of Twente (UT) has entered the new decade with an ambitious, new vision, mission and strategy. As ‘the ultimate people-first university of technology' we are rapidly expanding on our High Tech Human Touch philosophy and the unique role it affords us in society. Everything we do is aimed at maximum impact on people, society and connections through the sustainable utilisation of science and technology. We want to contribute to the development of a fair, digital and sustainable society through our open, inclusive and entrepreneurial attitude. This attitude permeates everything we do and is present in every one of UT's departments and faculties. Building on our rich legacy in merging technical and social sciences, we focus on five distinguishing research domains: Improving healthcare by personalised technologies; Creating intelligent manufacturing systems; Shaping our world with smart materials; Engineering our digital society; and Engineering for a resilient world.

As an employer, University of Twente offers jobs that matter. We equip you as a staff member to shape new opportunities both for yourself and for our society. With us, you will be part of a leading tech university that is changing our world for the better. We offer an open, inclusive and entrepreneurial climate, in which we encourage you to make healthy choices, for example, with our flexible, customisable conditions.

[Jmlspecs-interest] Android

[Zach L. <za...@in...>]

I am interested in formal methods and I was thinking of adding specs to an
existing open-source Android application.

However, a cursory search mainly turned up discussion indicating that
OpenJML had issues with Android's use of async.  I got the impression that
OpenJML is not well supported on the platform; that I might be able to use
it to verify classes in isolation but that it would be problematic to fit
into an existing workflow.

Any advice for using OpenJML or KeY on Android?

Thank you,
-Zach Lym

[Jmlspecs-interest] PhD positions in the Dynamic Analysis Group - Faculty of Informatics - Università della Svizzera italiana (USI), Lugano, Switzerland

[Andrea R. <and...@us...>]

The Dynamic Analysis Group in the Faculty of Informatics at Università della Svizzera italiana (USI) is looking for excellent applications to fill open positions for PhD students. Successful applicants will pursue a PhD under the supervision of Prof. Walter Binder and Dr. Andrea Rosà. The topic of the doctoral dissertation is flexible (to be defined based on individual research interests) and can span a wide spectrum of topics in the field of software engineering and programming languages, including (but not limited to): parallel and concurrent programming; managed languages and runtimes; language-integrated queries; big-data; query optimization; compilers; speculative dynamic compiler optimizations; monitoring, analysis and optimization; benchmarking.

-- Your profile

We are looking for enthusiastic, highly motivated, and excellent applicants with an MSc degree in Computer Science (or close to completing the MSc studies).
The candidates should have a thorough background and experience in at least one mainstream programming languages (e.g., Java, Scala, JavaScript, Python, Rust, C/C++) as well as excellent programming and algorithmic-thinking skills.

-- What we offer

At USI, PhD salaries are highly competitive, in accordance with Swiss standards. Salary is guaranteed for the whole duration of the PhD, which can last up to 5 years. Research equipment and travel funds are provided.

-- How to apply

If you are interested, send your application to both wal...@us...<mailto:wal...@us...> and and...@us....
Applications should include a Curriculum Vitae (including one or two references) and a course transcript. The call will remain open until all positions are filled. It is strongly advised to apply as soon as possible.


------------
Andrea Rosà
Postdoctoral Researcher
Faculty of Informatics - Office SI-205
Università della Svizzera italiana (USI)
Via G. Buffi 13
CH-6904 Lugano
Switzerland
(e) and...@us...
(p) +41 58 666 4455 ext. 2183
(w) http://www.inf.usi.ch/phd/rosaa/

[Jmlspecs-interest] OpenJML with two or more classes

[Gualter P. <g.p...@ca...>]

Hello,

I hope this is the correct place to ask this question.

I have verified both the following pieces of code using OpenJML:

public class Customer {

    /*@ public invariant this.customerID != 0; */
    /*@ public invariant this.customerID >= -1; */
    /*@ spec_public */ private int customerID;
    /*@
    @ public normal_behavior
    @ requires customerID != 0;
    @ requires customerID >= -1;

    @*/
    public Customer(int customerID) {
        this.customerID = customerID;
    }

    /*@
    @ public normal_behavior
    @ requires true;
    @*/
    public int getId() {
        return customerID;
    }

    /*@
    @ also
    @ public normal_behavior // Generated by Daikon
    @ requires true;
    @*/
    public String toString() {
        return "I am customer with ID " + customerID + ".";
    }
}

public class Order {

    /*@ public invariant this.orderID != 0; */
    /*@ public invariant this.orderID >= -1; */
    /*@ spec_public */ private int orderID;

    /*@
    @ public normal_behavior
    @ requires orderID != 0;
    @ requires orderID >= -1;
    @*/
    public Order(int orderID) {
        this.orderID = orderID;
    }

    /*@
    @ public normal_behavior
    @ requires true;
    @*/
    public int getOrderID() {
        return orderID;
    }
}

and I obtain no warnings. I ran *java -jar openjml.jar -esc
examples/Customer.java *and* java -jar openjml.jar -esc
examples/Order.java*. The folder examples contains both files
Customer.java and Order.java.

However, when I change Customer.java to include now an object Order, like this:

public class Customer {

    /*@ public invariant this.customerID != 0; */
    /*@ public invariant this.customerID >= -1; */
    /*@ public invariant this.order != null; */
    /*@ public invariant this.order.orderID != 0; */
    /*@ public invariant this.order.orderID >= -1; */
    /*@ spec_public */ private int customerID;
    /*@ spec_public */ private Order order;

    /*@
    @ public normal_behavior
    @ requires customerID != 0;
    @ requires customerID >= -1;
    @ ensures this.order.orderID == -1;
    @*/
    public Customer(int customerID) {
        this.customerID = customerID;
        this.order = new Order(-1);
    }

    /*@
    @ public normal_behavior
    @ requires true;
    @*/
    public int getId() {
        return customerID;
    }

    /*@
    @ public normal_behavior
    @ ensures this.customerID == \old(this.customerID);
    @ ensures this.order == \result;
    @ ensures this.order.orderID == \result.orderID;
    @ ensures \result == \old(this.order);
    @ ensures \result.orderID == \old(this.order.orderID);
    @ ensures \result != null;
    @*/
    public Order getOrder() {
        return order;
    }

    /*@
    @ public normal_behavior
    @ requires this.order.orderID == -1;
    @ requires o != null;
    @ requires this.order != null ==> o != null;
    @ requires this.order.orderID < o.orderID;
    @ ensures this.customerID == \old(this.customerID);
    @ ensures this.order == \old(o);
    @ ensures this.order.orderID == o.orderID;
    @ ensures o.orderID == \old(o.orderID);
    @ ensures this.order != null ==> \old(this.order) != null;
    @ ensures o.orderID > \old(this.order.orderID);
    @*/
    public void setOrder(Order o){
        this.order = o;
    }

    /*@
    @ also
    @ public normal_behavior
    @ requires true;
    @*/
    public String toString() {
        return "I am customer with ID " + customerID + ".";
    }
}

after executing *java -jar openjml.jar -esc -dir examples*, I obtain the
following warnings:

examples/Customer.java:17: warning: The prover cannot establish an
assertion (InvariantExit: examples/Customer.java:4: ) in method
Customer
    public Customer(int customerID) {
           ^
examples/Customer.java:4: warning: Associated declaration:
examples/Customer.java:17:
    /*@ public invariant this.customerID >= -1; */
               ^

examples/Customer.java:17: warning: The prover cannot establish an
assertion (InvariantExit: examples/Customer.java:3: ) in method
Customer
    public Customer(int customerID) {
           ^
examples/Customer.java:3: warning: Associated declaration:
examples/Customer.java:17:
    /*@ public invariant this.customerID != 0; */
               ^

examples/Customer.java:17: warning: The prover cannot establish an
assertion (Postcondition: examples/Customer.java:15: ) in method
Customer
    public Customer(int customerID) {
           ^
examples/Customer.java:15: warning: Associated declaration:
examples/Customer.java:17:
    @ ensures this.order.orderID == -1;
      ^
6 warnings

I am not able to understand why this happens.

Thank you,

Gualter

[Jmlspecs-interest] VTLTC 2020 - Final Call for Online Participation

[<r.e...@ut...>]

                    Final Call for Online Participation

                 VerifyThis Long-Term Challenge 2020

                -- Online Result and Exchange Event --

                      27th April 2020, 10:00 UTC [0]

         >>> https://verifythis.github.io/online-event <<<


!! Please register on this website if you want to participate
!! (There are no costs involved in participating)


## Introduction
 
The VerifyThis Long-Term Challenge complements the on-site format of
the VerifyThis competition with a verification challenge, in which
teams contribute to the verification of a practically relevant piece
of software over a longer period of time. The challenge aims to be a
showcase that deductive program verification can produce relevant
results for real systems with acceptable effort.

The challenge system to be verified is the new implementation of the
PGP server infrastructure, called HAGRID [2]. The old implementation
did not conform to GDPR and was known to be vulnerable against DoS
attacks.


## The Online Result and Exchange Workshop

A final workshop session for the challenge had been planned at ETAPS
(along with the VerifyThis program verification competition [1]).
Since ETAPS has been postponed, we will meet and exchange online.

We have received five submissions that each contribute a solution to
different aspects of the challenge using different abstractions,
different assumptions and different verification techniques.

During this online meeting, the different solutions will be briefly
explained, and we discuss the approaches, how they can benefit from
one another and how further verification success can be stipulated.

This meeting is not meant as a replacement of the on-site event. It is
meant as an informal event to exchange ideas, to give positive
impulses on further advances of approaches, or on how to combine
solutions. If the situation permits, the onsite event will take place
in autumn during ETAPS.

## Call for Participation

Everybody who is interested about the challenge, the proposed
solutions and VerifyThis is cordially invited to join the meeting! To
avoid spammers, you need to register yourself. An email with login
credentials will be sent in advance. Registration information, agenda
and resources are on our webpage of the online workshop:

          >>> https://verifythis.github.io/online-event <<<



## Agenda

We start at 10:00 UTC. Please join the meeting in-time.

1. Greeting and Introduction to the VerifyThis Longterm Challenge 2020

2. Claire Dross, Johannes Kanig, and Yannick Moy
   A Solution to the Long-Term Challenge in SPARK

3. Diego Diverio, Cláudio Lourenço and Claude Marché
   ``You-Know-Why'': an Early-Stage Prototype of a Key Server
   Developed using Why3

4. Stijn de Gouw, Mattias Ulbrich and Alexander Weigl
   The KeY Approach on Hagrid

5. Gidon Ernst and Lukas Rieger
   Information Flow Testing of a PGP Keyserver

6. Gidon Ernst, Toby Murray and Mukesh Tiwari
   Verifying the Security of a PGP Keyserver

7. Final discussion and feedback to the challenge.

8. Closing (ca. 14:00)


## Program Chairs and Organizers

Marieke Huisman                 Raul E. Monti

Mattias Ulbrich                 Alexander Weigl


[0] Find out your local time here:
    https://www.timeanddate.com/worldclock/fixedtime.html?msg=VerifyThis%20Online&iso=20200427T12&p1=964&ah=3

[1] https://www.pm.inf.ethz.ch/research/verifythis.html

[2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/

[Jmlspecs-interest] VTLTC 2020 - Call for Online Participation

[<r.e...@ut...>]

                    Call for Online Participation.


                 VerifyThis Long-Term Challenge 2020

                -- Online Result and Exchange Event --

                   27th April 2020, 10:00 UTC [0]

           >>> https://verifythis.github.io/online-event <<<



## Introduction

The VerifyThis  Long-Term Challenge complements the  on-site format of
the  VerifyThis competition  with a  verification challenge,  in which
teams contribute to  the verification of a  practically relevant piece
of software over a  longer period of time. The challenge  aims to be a
showcase  that deductive  program  verification  can produce  relevant
results for real systems with acceptable effort.

The challenge system  to be verified is the new  implementation of the
PGP server  infrastructure, called HAGRID [2].  The old implementation
did not  conform to GDPR  and was known  to be vulnerable  against DoS
attacks.


## The Online Result and Exchange Workshop

A final workshop  session for the challenge had been  planned at ETAPS
(along  with the  VerifyThis  program  verification competition  [1]).
Since ETAPS has been postponed, we will meet and exchange online.

We have received  five submissions that each contribute  a solution to
different  aspects  of  the challenge  using  different  abstractions,
different assumptions and different verification techniques.

During this  online meeting, the  different solutions will  be briefly
explained, and  we discuss the  approaches, how they can  benefit from
one another and how further verification success can be stipulated.

This meeting is not meant as a replacement of the on-site event.  It
is meant as an informal event to exchange ideas, to give positive
impulses on further advances of approaches, or on how to combine
solutions. If the situation permits, the onsite event will take place
in autumn during ETAPS.


## Call for Participation

Everybody  who  is  interested   about  the  challenge,  the  proposed
solutions and VerifyThis is cordially invited to join the meeting!


## Online Link

More information on how to participate, agenda and resources are on
our webpage of the online workshop:

           >>> https://verifythis.github.io/online-event  <<<


## Program Chairs and Organizers

Marieke Huisman                 Raul E. Monti

Mattias Ulbrich                 Alexander Weigl


[0] Find out your local time here:
https://www.timeanddate.com/worldclock/fixedtime.html?msg=VerifyThis&iso=2020-04-27T10:00:00

[1] https://www.pm.inf.ethz.ch/research/verifythis.html

[2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/

[Jmlspecs-interest] CFP for VerifyThis Long-Term Challenge (VTLTC 2020)

[<r.e...@ut...>]

                          Call for Presentations



                     VerifyThis Long-Term Challenge 2020

                            - Concluding Event -



                    co-located with ETAPS and VerifyThis

                  25th and 26th April 2020, Dublin, Ireland

                        http://verifythis.github.io/



                          Deadline: 1st March 2020



## Introduction



The VerifyThis  Long-Term Challenge complements the  on-site format of

the  VerifyThis competition  with a  verification challenge,  in which

teams contribute to  the verification of a  practically relevant piece

of software over  a period of six  months. The challenge aims  to be a

showcase  that deductive  program  verification  can produce  relevant

results for  real systems with  acceptable effort. The  challenge 2020

started in  September 2019, and  ends February 2020.  To  conclude the

challenge, we will  have a final workshop session at  ETAPS along with

the VerifyThis program verification competition [1].



For 2020, the  challenge system is the new, implementation  of the PGP

server infrastructure,  called HAGRID [2]. The  old implementation did

not  conform to  GDPR  and  was known  to  be  vulnerable against  DoS

attacks.



We invite  you to  present your  results on  the verification  of this

security-relevant  challenge system  during a  special session  of the

VerifyThis program verification competition, held at ETAPS.



## Submission



Authors are invited to submit a presentation proposal (or extended

abstract) as a PDF using Springer’s LNCS style, which should be about

a page long, but not longer than three pages (excluding bibliography).

It should discuss ...



* ... the used verification approach and tools

* ... how the challenge was adapted to make verification possible

  (abstractions, reimplementation, different behaviour)

* ... what has been achieved (modelled and verified properties)

* ... successes and challenges encountered in the course of the case

  study.



## Submission Link



https://easychair.org/conferences/?conf=vtltc2020



## Proceedings



There will be an informal pre-proceeding of the accepted presentation

proposals.



A special issue for this verification challenge is planned and will be

discussed on-site.



## Important dates



Submission deadline: 1st March 2020

Notifications: 15th March 2020

Workshop: 25-26th April 2020



## Program Chairs and Organizers



Marieke Huisman                 Raul E. Monti

Mattias Ulbrich                 Alexander Weigl





[1] https://www.pm.inf.ethz.ch/research/verifythis.html

[2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/

[Jmlspecs-interest] 3d Call for Papers F-IDE Workshop 2019 (Extended Deadlines)

[cok <co...@fr...>]

Apologies if you already received this through other channels:


F-IDE - 5th Workshop on Formal Integrated Development Environments

https://fideworkshop2019inesctec.pt <https://fideworkshop2019.inesctec.pt/>

part of FM Week 2019 (http://formalmethods2019.inesctec.pt/?page_id=84 <http://formalmethods2019.inesctec.pt/?page_id=84>)

# News

We are happy to announce that Wolfgang Ahrendt (Chalmers University) accepted to give the opening keynote at F-IDE 2019.

# Important Dates

- Abstract submission: July 2, 2019 (extended)
- Paper submission: June 9, 2019 (extended)
- Notification: August 20, 2019
- Camera-ready version: September 3, 2019
- Workshop date: October 7, 2019

# About F-IDE

High levels of safety, security and also privacy standards require the
use of formal methods to specify and develop compliant software
(sub)systems. Any standard comes with an assessment process, which
requires a complete documentation of the application to ease the
justification of design choices and the review of code and proofs.

Ideally, an F-IDE dedicated to such developments should comply with
several requirements. The first one is to associate a logical theory
with a programming language, in a way that facilitates the tightly
coupled handling of specification properties and program constructs. The
second is to offer a language/environment simple enough to be usable by
most developers, even if they are not fully acquainted with higher-order
logics or set theory, in particular by making development of proofs as
easy as possible. The third is to offer automated management of
application documentation. It may also be expected that developments
done with such an F-IDE are reusable and modular. Tools for testing and
static analysis may be embedded within F-IDEs to support the assessment
process.

# Submission Guidelines

Submitted papers should follow EPTCS format (http://style.eptcs.org/ <http://style.eptcs.org/>).
Authors are invited to submit the following types of contributions:

    Research papers providing new concepts and results
    Experience reports
    Position papers and research perspectives
    Tool presentations

Two kinds of submissions will be considered: normal paper (15 pages
including bibliography), and shorter papers describing work in progress
and preliminary results (6 pages including bibliography). Submissions
will be made through EasyChair at:

https://easychair.org/conferences/?conf=fide2019 <https://easychair.org/conferences/?conf=fide2019>.

All papers will be peer-reviewed by at least two members of the program
committee. They must describe original contributions whose main results
and conclusions have not been published or submitted elsewhere.
Preliminary proceedings, including all the papers selected for the
workshop, will be available electronically at the workshop Post
proceedings will be proposed for publication with Electronic Proceedings
in Theoretical Computer Science (EPTCS).

# List of Topics

The workshop is open to contributions on all aspects of a system
development process, including specification, design, implementation,
analysis and documentation. It welcomes the presentation of tools,
methods, techniques and experiments. Topics of interest include, but are
not limited to, the following:

    F-IDE building: design and integration of languages, 
    development of user-friendly front-ends
    How to make high-level logical and programming concepts palatable
    to industrial developers
    Integration of Object-Oriented and modularity features
    Integration of static analyzers
    Integration of automatic proof tools,
    theorem provers and testing tools
    Documentation tools
    Impact of tools on certification
    Experience reports on developing F-IDEs
    Experience reports on using F-IDEs
    Experience reports on formal methods-based assessments
    in industrial applications

# Committees
## PC Co-Chairs

    Rosemary Monahan, Maynooth University, rosemary (dot) monahan (at)
nuim (dot) ie
    Virgile Prevosto, Institut List, CEA Tech, Université Paris-Saclay,
virgile (dot) prevosto (at) cea (dot) fr
    José Proença, HASLab/INESC-TEC and Universidade do Minho, jose (dot)
p (dot) proenca (at) inesctec (dot) pt

## Steering Committee

    Catherine Dubois, Samovar / ENSIIE, catherine (dot) dubois (at)
ensiie (dot) fr
    Paolo Masci, HASLab/INESC-TEC and Universidade do Minho, paolo (dot)
masci (at) inesctec (dot) pt
    Dominique Méry, LORIA / Université de Lorraine, dominique (dot) mery
(at) loria (dot) fr

## Program Committee

    Cinzia Bernardeschi (University of Pisa)
    José Creissac Campos (University of Minho)
    Paul Curzon (Queen Mary University of London)
    Damien Doligez (INRIA)
    Andrea Domenici (University of Pisa)
    Carlo A. Furia (Chalmers University of Technology)
    Kenneth Lausdahl (Aarhus University)
    Stephan Merz (Inria Nancy)
    Stefan Mitsch (Carnegie Mellon University)
    Yannick Moy (Adacore)
    César Muñoz (NASA Langley)
    Andrei Paskevich (Université Paris-Sud, LRI)
    François Pessaux (ENSTA ParisTech)
    James Power (Maynooth University)
    Steve Reeves (University of Waikato)
    Bernhard Rumpe (RWTH Aachen University)
    Claudio Sacerdoti-Cohen (University of Bologna)
    Silvia Lizeth Tapia Tarifa (University of Oslo)
    Mattias Ulbricht (Karlsruhe Institute of Technology)
    Laurent Voisin (Systerel)
    Makarius Wenzel (sketis.net <http://sketis.net/>)
    Yi Zhang (U.S. Food and Drug Administration)

# Venue

The conference will be held in Porto (Portugal), as part of FM Week 2019

# Contact

All questions about submissions should be emailed to the PC co-chairs
(see contact information above).


-- 
E tutto per oggi, a la prossima volta
Virgile
_______________________________________________
Why3-club mailing list
Why...@li... <mailto:Why...@li...>
https://lists.gforge.inria.fr/mailman/listinfo/why3-club <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>

[Jmlspecs-interest] 2 PhD positions on the ChEOPS project in Twente and Eindhoven

[<m.h...@ut...>]

University of Twente
Formal Methods and Tools (FMT)
Contact: Prof.Dr. Marieke Huisman (m.h...@ut...)

Eindhoven University of Technology
Software Engineering & Technology (SET)
Contact: Dr. Ing. Anton Wijs (a.j...@tu...)
JOB DESCRIPTION
We are seeking two PhD students to work on the ChEOPS project, a collaborative project between the universities of Twente and Eindhoven, funded by the Open Technology Programme of the NWO Applied and Engineering Sciences (TTW) domain.
In the ChEOPS project, research is conducted to make the development and maintenance of software aimed at graphics processing units (GPUs) more insightful and effective in terms of functional correctness and performance. GPUs have an increasingly big impact on industry and academia, due to their great computational capabilities. However, in practice, one usually needs to have expert knowledge on GPU architectures to optimally gain advantage of those capabilities.

At the Eindhoven University of Technology, we work on modelling GPU applications using a Domain Specific Language (DSL), formally verifying the correctness of the models, and automatically generating GPU code. At the University of Twente, we work on the structured optimisation of GPU code, while ensuring that functional correctness is preserved. Existing formal verification techniques, model checking and code verification, are combined to create, for the first time, a complete end-to-end development workflow for GPU applications.

Two PhD positions are available to work on the following subprojects:

SUBPROJECT 1 (Eindhoven): DSLs for the design of GPU applications. This subproject involves the functional verification of the resulting models, as well as model-to-code generation.

SUBPROJECT 2 (Twente): Building model-to-code generation, and the verification of optimisations in the form of code-to-code transformations.

We expect the two PhD students to collaborate closely within the project. In addition, there will be ample interaction with the members of the Model Driven Engineering section in Eindhoven on the model-to-code generation, and with the team building the VerCors tool set for verification of concurrent software in Twente.
For more information about the concrete subprojects, please contact Marieke Huisman: m.h...@ut... or Anton Wijs: a.j...@ut....
We seek two PhD students with an MSc degree (or equivalent) in Computer Science.
The candidates should be enthusiastic, and have a thorough theoretical background, a demonstrable interest in DSLs and model checking (subproject 1) or program verification (subproject 2), and knowledge about multithreaded programming (at least in Java/C/C++, experience with GPU programming is a plus).
We are looking for researchers with an independent mind who are willing to cooperate in our team. It is understood that he or she works on the topics listed above.  Furthermore, we ask for good communicative and collaboration skills. Candidates should be prepared to prove their English language skills.
As a research outcome we expect publications, (prototype) tools, and a PhD thesis.
Intended starting date of the position: September 1, 2019.
We offer
- Two PhD position for four years (38 hrs/week).
- A stimulating scientific environment.
- Full status as an employee at the University of Twente, or the Eindhoven University of Technology,  including pension and health care benefits.
- Gross salary PhD student: ranging from € 2.191,00 (1st year) to € 2.801,00 (4th year) per month, plus holiday allowance (8%) and end-of-year bonus (8.3%).
- Excellent facilities for professional and personal development, such as the possibility to attend courses, summer schools, conferences etc.
- Good secondary conditions, in accordance with the collective labour agreement CAO-NU for Dutch universities.
- In Twente: A green Campus with lots of sports facilities.
- In Eindhoven: A campus with great sports facilities, with the Eindhoven city center within walking distance.
The PhD student in Twente will be a member of the Twente Graduate School in the research programme 'Dependable and Secure Computing'. Their research programme offers advanced courses to deepen your scientific knowledge in preparation to your future career (within or outside academia). In Eindhoven, the PhD student will be able to follow such courses in the PROOF (PROviding Opportunities For PhD students) programme. We provide our PhD students with excellent opportunities to broaden their personal knowledge and to professionalise their academic skills. Participation in national and/or international summer schools and workshops, and visits to other prestigious research institutes and universities can be part of this programme.
FURTHER INFORMATION
- FMT group: http://fmt.cs.utwente.nl/
- SET group: https://www.tue.nl/en/research/research-groups/software-engineering-and-technology/
- Prof.Dr. Marieke Huisman (M.H...@ut...): http://wwwhome.cs.utwente.nl/~marieke/
- Dr.Ing. Anton Wijs (a.j...@tu...): https://www.win.tue.nl/~awijs/
- Project webpage: https://fmt.ewi.utwente.nl/research/projects/view/CheOPS/
APPLICATION
To apply for the PhD position directly, follow this link:
https://www.utwente.nl/en/organization/careers/!/685937/2-phd-positions-on-the-cheops-project-in-twente-and-eindhoven-netherlands-verified-construction-of-correct-and-optimized-parallel-software
Please use the Apply Now button at the bottom of the page.
Deadline: July 1, 2019, or until the positions are filled. Earlier applications are welcome.

Your application should consist of:
- a cover letter (explaining your specific interest and qualifications); if applicable also indicate whether you prefer the position in Twente or Eindhoven
- a full Curriculum Vitae; this should include a list of all courses + marks, and a short description of your MSc thesis;
- references (contact information) of two scientific staff members.

[Jmlspecs-interest] Postdoc position on the Mercedes project in Twente (Netherlands): Maximal Reliability of Concurrent and Distributed Software

[<m.h...@ut...>]

Postdoc position on the Mercedes project in Twente (Netherlands):
Maximal Reliability of Concurrent and Distributed Software

University of Twente
Group: Formal Methods and Tools
Contact: Prof. Dr. Marieke Huisman (m.h...@ut...<mailto:m.h...@ut...>)

Job Description
You will be working on the Mercedes project, a 1,5 million euro personal grant for Marieke Huisman, funded by NWO.

Goal of the Mercedes project is to develop techniques to ensure the maximal reliability of concurrent and distributed software. In earlier projects, we started working on the development of a tool set for the verification of concurrent programs, called VerCors which is a result of Marieke Huisman’s earlier ERC project on verification of concurrent software. The VerCors tool set uses deductive program verification, i.e., the desired program properties are written in a pre-postcondition style (using a form of separation logic).

The focus of this Postdoc project will be on enabling verification of large programs with a significant concurrent aspect. Your ideas would be implemented in or should be applicable to the VerCors tool set. We value contributions to the theory of large-scale verification, to the process in which verification can be applied to large-scale software projects, and/or to the implementation of features that may have a significant impact on the usability of VerCors in the context of large scale verification.

For more information about the concrete project, please contact Marieke Huisman (m.h...@ut...<mailto:m.h...@ut...>).

We seek
We are looking for a researcher with an independent mind who is willing to cooperate in our team. It is understood that he or she works on the topics listed above. Further we ask for good communicative and collaboration skills. Candidates should be prepared to prove their English language skills.

As a research outcome we expect publications and (prototype) tools.

We offer
- One post doc position for two years (38 hrs/week), with a possibility of extension of upto 2 more years.
- A stimulating scientific environment
- Full status as an employee at the University of Twente, including pension and health care benefits.
- Gross salary for a Postdoc is dependent on experience and background, but will minimally be € 3.068,00 per month (scale 10.4), plus holiday allowance (8%) and end-of-year bonus (8.3%).
- Excellent facilities for professional and personal development.
- Good secondary conditions, in accordance with the collective labour agreement CAO-NU for Dutch universities
- A green Campus with lots of sports facilities

Further information
- FMT group: http://fmt.cs.utwente.nl/
- Prof. Dr. Marieke Huisman (M.H...@ut...)<mailto:M.H...@ut...)>: http://wwwhome.cs.utwente.nl/~marieke/
- Project webpage: http://fmt.ewi.utwente.nl/research/projects/Mercedes/

Application
To apply for the button, visit
https://www.utwente.nl/en/organization/careers/vacancy/!/423176/postdoc-position-on-the-mercedes-project-on-maximal-reliability-of-concurrent-and-distributed-software

Please use the Apply Now button at the bottom of the page.

Deadline: November 24, 2018. Earlier applications are welcome and an early start date is an advantage.

Your application should consist of:

- a cover letter (explaining your specific interest and qualifications);
- a full Curriculum Vitae,
  to apply for the PhD student position, this should include a list of
  all courses + marks, and a short description of your MSc thesis;
  to apply for the post doc position, this should include a list of
  all publications, and a short description of your PhD thesis;
- references (contact information) of two scientific staff members.

[Jmlspecs-interest] Call for Papers: ManLang 2018 (Sept. 10-14, Linz, Austria)

[ManLang C. <ma...@jk...>]

------------------------------------------------------------------------------------------------

CALL FOR PAPERS

15th International Conference on Managed Languages & Runtimes
(ManLang'18)

September 10-14, 2018, Linz, Austria

http://ssw.jku.at/manlang18/ 

------------------------------------------------------------------------------------------------

ManLang (formerly PPPJ) is a premier forum for presenting and discussing
novel results in all aspects of managed programming languages and
runtime systems, which serve as building blocks for some of the most
important computing systems, ranging from small-scale (embedded and
real-time systems) to large-scale (cloud-computing and big-data
platforms) and anything in between (mobile, IoT, and wearable
applications).

======
Topics
======

Topics of interest include but are not limited to:

Languages and Compilers
-----------------------
- Managed languages (e.g., Java, Scala, JavaScript, Python, Ruby, C#,
F#, Clojure, Groovy, Kotlin, R, Smalltalk, Racket, Rust, Go, etc.)
- Domain-specific languages
- Language design
- Compilers and interpreters
- Type systems and program logics
- Language interoperability
- Parallelism, distribution, and concurrency

Virtual Machines
----------------
- Managed runtime systems (e.g., JVM, Dalvik VM, Android Runtime (ART),
LLVM, .NET CLR, RPython, etc.)
- VM design and optimization
- VMs for mobile and embedded devices
- VMs for real-time applications
- Memory management
- Hardware/software co-design

Techniques, Tools, and Applications
-----------------------------------
- Static and dynamic program analysis
- Testing and debugging
- Refactoring
- Program understanding
- Program synthesis
- Security and privacy
- Performance analysis and monitoring
- Compiler and program verification

===============
Important Dates
===============

Submission: May 4, 2018 (Abstracts: April 27)
Notification: July 6, 2018
Camera-ready version: August 3, 2018
Poster submission: August 6, 2018
Poster notification: August 13, 2018
Conference: September 10-14, 2018

==========================
Submission and Proceedings
==========================

Submissions to the conference will be evaluated on the basis of
originality, relevance, technical soundness and presentation quality.
Papers should be written in English and not exceed 12 pages in ACM
format for full papers (6 pages for WiP, industry, and tool papers). You
can also submit posters, which can be accompanied by a one-page
abstract, and are due on August 6, 2018. The conference proceedings will
be published as part of the ACM International Conference Proceedings
Series and will be disseminated through the ACM Digital Library.

See the conference homepage for details on paper formats and submission.

============
Organization
============

General Chair:
Hanspeter Mössenböck, Johannes Kepler University Linz, Austria

Program Chair:
Eli Tilevich, Virginia Tech, USA

Steering Committee:
Walter Binder, University of Lugano (USI), Switzerland
Bruce Childers, University of Pittsburgh, USA
Martin Pluemicke, DHBW Stuttgart, Germany
Christian Probst, Technical University of Denmark, Denmark
Petr Tuma, Charles University, Czech Republic
Thomas Würthinger, Oracle Labs, Switzerland

Program Committee:
Godmar Back, Virginia Tech, USA
Clement Bera, INRIA, France
Christoph Bockisch, Philipps Universität Marburg, Germany
Man Cao, Google, USA
Shigeru Chiba, University of Tokyo, Japan
Yvonne Coady, University of Victoria, Canada
Julian Dolby, IBM Research, USA
Patrick Eugster, University of Lugano, Switzerland
Irene Finocchi, Sapienza University of Rome, Italy
Görel Hedin, Lund University, Sweden
Robert Hirschfeld, Hasso Plattner Institute, Germany
Tony Hosking, Purdue University, USA
Doug Lea, SUNY Oswego, USA
Eliot Moss, University of Massachusetts, USA
Nate Nystrom, University of Lugano, Switzerland
Tiark Rompf, Purdue University, USA
Jennifer B. Sartor, Vrije Universiteit Brussel, Belgium
JeremyJan Vitek, Northeastern University, USA
Christian Wimmer, Oracle Labs, USA
Jianjun Zhao, Kyushu University, Japan

========
Location
========

Linz, the capital of Upper Austria, is both a city of culture and of
industry. Located at the Danube it features a historic downtown and a
modern university campus just north of the Danube, where the conference
will take place. For information on JKU and Linz, also see:
http://www.jku.at, https://en.wikipedia.org/wiki/Linz and
https://www.linz.at/english/ 

=================
Other Information
=================

The 5th Virtual Machine Meetup (VMM) is a collocated event with ManLang
'18. It is a venue for discussing the latest research and developments
in the area of managed language execution.

ManLang'18 is organized in cooperation with ACM, ACM SIGPLAN and ACM
ICPS, and is sponsored by the JKU Department of Computer Science, Oracle
Labs, and Linz AG.

http://ssw.jku.at/manlang18/ 
https://www.facebook.com/ManLangConf/ 
https://twitter.com/manlangconf

[Jmlspecs-interest] Survey About Specification Preferences

[Gary T. L. <le...@ee...>]

Hi,

In work that John Singleton, Hridesh Rajan, and I are doing, we would like
you to take a survey about your preferences regarding some pairs of JML
specifications. The data will all be anonymously collected. If you have 10
minutes or so, please take the survey, as that will help our research.  The
survey is at

http://ucf.qualtrics.com/jfe/form/SV_88k5ySHbhZt0f1H

        Regards,

        Gary T. Leavens
        437D Harris Center (Bldg. 116)
        Computer Science, University of Central Florida
        4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
        http://www.cs.ucf.edu/~leavens <http://www.eecs.ucf.edu/~leavens>
phone: +1-407-823-4758
        le...@cs... <le...@ee...>

Re: [Jmlspecs-interest] progress core language

[Dr. J. J. H. <jj...@ai...>]

Dear Gary,

I doubt if I could make a meeting in Florida so late in December.

Sincerely,
James

On 06/07/2017 07:29 PM, Gary T. Leavens wrote:
> Hi,
>
> Let me first apologize for not doing more to organize the next JML
> meeting (and also not much on other JML work...). I recall the plan
> was for December 2017 in Orlando, Florida, and I had thought we had
> already had some discussion about the dates. However, I can't find
> those emails...  So let's start again.
>
> To have the event on the UCF campus, it would be ideal to have it
> after December 16, 2017, as that is the end of commencement exercises
> for fall here at UCF.  The other constraint is Christmas (Dec. 25).
> Would it work to have our meeting on December 18-20?  Let me know and
> I can check on facilities to hold the meeting.
>
>         Regards,
>
>         Gary T. Leavens
>         437D Harris Center (Bldg. 116)
>         Computer Science, University of Central Florida
>         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
>         http://www.cs.ucf.edu/~leavens
> <http://www.eecs.ucf.edu/%7Eleavens>  phone: +1-407-823-4758
>         le...@cs... <mailto:le...@ee...>
>
> On Tue, Jun 6, 2017 at 5:58 PM, Mattias Ulbrich <ul...@ki...
> <mailto:ul...@ki...>> wrote:
>
>     Hi everybody,
>
>     On 04/28/2017 09:34 AM, m.h...@ut...
>     <mailto:m.h...@ut...> wrote:
>     > And have we agreed on the dates for a meeting in Florida? It
>     would be
>     > good to announce this as well, so people can save the date.
>
>     I would like to reraise this question since I have got another
>     appointment request for the beginning of December.
>
>     Best, Mattias
>
>     --
>     Dr. Mattias Ulbrich <ul...@ki... <mailto:ul...@ki...>>
>     Application-oriented Formal Verification (Prof. B. Beckert)
>     Institut of Theoretical Informatics      formal.iti.kit.edu
>     <http://formal.iti.kit.edu>
>     KIT - Karlsruhe Institute of Technology         www.kit.edu
>     <http://www.kit.edu>
>
>


-- 
Dr. James J. Hunt     * CEO & Geschäftsführer * Tel: +49 721 663968 22

aicas GmbH
Emmy-Noether-Straße 9 * D-76131 Karlsruhe     * Deutschland (Germany)
http://www.aicas.com  * Tel: +49 721 663968 0 * FAX: +49 721 663968 99

USt-Id: DE216375633, Handelsregister HRB 109481, AG Mannheim
Geschäftsführer: Dr. James J. Hunt

aicas incorporated
6 Landmark Sq., Ste 400 * Stamford, CT 06901    * USA
http://www.aicas.com    * Tel: +1 203 435 0521

Re: [Jmlspecs-interest] progress core language

[<m.h...@ut...>]

That would work for me. Marieke

On 07/06/2017, 19:29, "gar...@gm...<mailto:gar...@gm...> on behalf of Gary T. Leavens" <gar...@gm...<mailto:gar...@gm...> on behalf of le...@ee...<mailto:le...@ee...>> wrote:

Hi,

Let me first apologize for not doing more to organize the next JML meeting (and also not much on other JML work...). I recall the plan was for December 2017 in Orlando, Florida, and I had thought we had already had some discussion about the dates. However, I can't find those emails...  So let's start again.

To have the event on the UCF campus, it would be ideal to have it after December 16, 2017, as that is the end of commencement exercises for fall here at UCF.  The other constraint is Christmas (Dec. 25). Would it work to have our meeting on December 18-20?  Let me know and I can check on facilities to hold the meeting.

        Regards,

        Gary T. Leavens
        437D Harris Center (Bldg. 116)
        Computer Science, University of Central Florida
        4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
        http://www.cs.ucf.edu/~leavens<http://www.eecs.ucf.edu/~leavens>  phone: +1-407-823-4758
        le...@cs...<mailto:le...@ee...>

On Tue, Jun 6, 2017 at 5:58 PM, Mattias Ulbrich <ul...@ki...<mailto:ul...@ki...>> wrote:
Hi everybody,

On 04/28/2017 09:34 AM, m.h...@ut...<mailto:m.h...@ut...> wrote:
> And have we agreed on the dates for a meeting in Florida? It would be
> good to announce this as well, so people can save the date.

I would like to reraise this question since I have got another
appointment request for the beginning of December.

Best, Mattias

--
Dr. Mattias Ulbrich <ul...@ki...<mailto:ul...@ki...>>
Application-oriented Formal Verification (Prof. B. Beckert)
Institut of Theoretical Informatics      formal.iti.kit.edu<http://formal.iti.kit.edu>
KIT - Karlsruhe Institute of Technology         www.kit.edu<http://www.kit.edu>

Re: [Jmlspecs-interest] progress core language

[Gary T. L. <le...@ee...>]

Hi,

Let me first apologize for not doing more to organize the next JML meeting
(and also not much on other JML work...). I recall the plan was for
December 2017 in Orlando, Florida, and I had thought we had already had
some discussion about the dates. However, I can't find those emails...  So
let's start again.

To have the event on the UCF campus, it would be ideal to have it after
December 16, 2017, as that is the end of commencement exercises for fall
here at UCF.  The other constraint is Christmas (Dec. 25). Would it work to
have our meeting on December 18-20?  Let me know and I can check on
facilities to hold the meeting.

        Regards,

        Gary T. Leavens
        437D Harris Center (Bldg. 116)
        Computer Science, University of Central Florida
        4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
        http://www.cs.ucf.edu/~leavens <http://www.eecs.ucf.edu/~leavens>
phone: +1-407-823-4758
        le...@cs... <le...@ee...>

On Tue, Jun 6, 2017 at 5:58 PM, Mattias Ulbrich <ul...@ki...> wrote:

> Hi everybody,
>
> On 04/28/2017 09:34 AM, m.h...@ut... wrote:
> > And have we agreed on the dates for a meeting in Florida? It would be
> > good to announce this as well, so people can save the date.
>
> I would like to reraise this question since I have got another
> appointment request for the beginning of December.
>
> Best, Mattias
>
> --
> Dr. Mattias Ulbrich <ul...@ki...>
> Application-oriented Formal Verification (Prof. B. Beckert)
> Institut of Theoretical Informatics      formal.iti.kit.edu
> KIT - Karlsruhe Institute of Technology         www.kit.edu
>
>