Welcome to the
Formal techniques can help analyze programs, precisely describe program behavior, and verify program properties. Languages such as Java, C#, and Scala are interesting targets for formal techniques due to their ubiquity and large installed base, stable and well-defined interfaces and platforms, powerful (but also complex) libraries. The rising deployment in smart cards and mobile computing raises concerns about security and demands new methods to counter new possibilities for abuse.
Work on formal techniques and tools and work on the formal underpinnings of programming languages themselves naturally complement each other. This workshop aims to bring together people working in both fields, on topics such as:
- Language semantics
- Specification techniques and languages
- Verification of program properties
- Verification logics
- Dynamic program analysis
- Static program analysis
- Type systems
The workshop welcomes a wide range of submissions, such as technical contributions, case studies, challenge proposals, and position papers. Just as the number and the feature set of Java-like languages is expanding, the term “Java-like” is also to be understood broadly.
For further details see call for papers.
With inquiries contact Vladimir Klebanov email@example.com
Call for Papers
Contributions are sought on open questions, new developments, or interesting new applications of formal techniques in the context of Java or similar languages. Contributions are possible in two formats:
- full papers (up to 6 pages in the ACM 2-column style)
- short papers (up to 2 pages in the ACM 2-column style)
Technical submissions should strive not merely to present completely finished work, but also raise challenging open problems or propose speculative new approaches. Case studies, reports from competitions, and other experience reports should identify lessons learned, reflect on the state of the art, or clearly motivate further research.
We particularly welcome (clearly marked) position and discussion papers that may simply present suitable topics for discussion at the workshop, or raise issues that you feel deserve the attention of the research community. Examples include future work identified from existing research, potential PhD proposals, and specific well-motivated challenges within the workshop scope.
Contributions will be formally reviewed for originality, relevance, and the potential to generate interesting discussions. Accepted papers will have the option of being published in the ACM Digital Library. In addition, depending on the nature of the contributions, we may be organizing a special journal issue as a follow-up to the workshop, as has been done for some of the previous FTfJP workshops. Contributions must be in English, in PDF format, and follow the format outlined above. Authors of accepted papers are required to ensure that at least one of them will be present at the workshop.
Submissions are expected via EasyChair: https://easychair.org/conferences/?conf=ftfjp2016
Please use the newest ACM LaTeX template.
- Werner Dietl (chair)
- Sophia Drossopoulou
- Gary T. Leavens
- Rustan Leino
- Rosemary Monahan
- Peter Müller
For information about the workshop series see http://ftfjp.bitbucket.org/
Paola Giannini, Elena Zucca and Marco Servetto
Coupling catch clauses with local declarations
Jonathan Hoyland and Matthew Hague
Generating Concurrency Checks Automatically
Gurvan Cabon, David Cachera and David Pichardie
An Extended Buffered Memory Model With Full Reorderings
Davide Ancona and Andrea Corradi
A formal account of SSA in Java-like languages
Davide Ancona, Francesco Dagnino and Elena Zucca
Towards a model of corecursion with default
Tomoyuki Aotani and Gary Leavens
Towards Modular Reasoning for Context-Oriented Programs
Timothy Jones and David Pearce
A Mechanical Soundness Proof for Subtyping Over Recursive Types
Sophia Drossopoulou, James Noble, Mark S Miller and Toby Murray
Permission and Authority Revisited towards a formalization
Jens Dietrich, Nicholas Hollingum and Bernhard Scholz
A Note on the Soundness of Difference Propagation
Partial solutions to VerifyThis 2016 challenges 2 and 3 using VeriFast
|Tue 19 Jul 2016updated|
|Sun 22 May 2016|
|Fri 22 Apr 2016updated|
Extended Submission deadline!
|Fri 15 Apr 2016|
Karlsruhe Institute of Technology
University of Genova
IRISA / University of Rennes 1
Julia SRL, Italy
Carlo A. Furia
Chalmers University of Technology
University of Warwick, UK
IRIF, Université Paris Diderot
MIT CSAIL, USA
Victoria University of Wellington
NASA Ames Research Center