13th International Conference on integrated Formal Methods (iFM 2017)

iFM 2017 Accepted Papers

James Baxter and Ana Cavalcanti. Algebraic Compilation of Safety-Critical Java Bytecode
Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif. Modular Verification of Order-Preserving Write-Back Caches
Mark Utting, David Pearce and Lindsay Groves. Making Whiley Boogie!
Stefan Blom, Saeed Darabi, Marieke Huisman and Wytse Oortwijn. The VerCors Tool Set: Verification of Parallel and Concurrent Software
Simone Silvetti, Alberto Policriti and Luca Bortolussi. An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
Andrii Kovalov, Elisabeth Lobe, Andreas Gerndt and Daniel Lüdtke. Task-Node Mapping in an Arbitrary Computer Network using SMT Solver
Yuting Chen and Carlo A. Furia. Triggerless Happy: Intermediate Verification with a First-Order Prover
Albert Rizaldi, Jonas Keinholz, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf and Tobias Nipkow. Formalising Traffic Rules for Autonomous Vehicles Involving Multiple Lanes in Isabelle/HOL
Fahrurrozi Rahman and Juliana Küster Filipe Bowles. Formal Verification of CNL Health Recommendations
Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi and Elena Pagani. Formal verification of ARP (Address Resolution Protocol) through SMT-based model checking - A case study -
Olaf Owe, Toktam Ramezanifarkhani and Elahe Fazeldehkordi. Hoare-style Reasoning from Multiple Contracts
Stephen Gilmore, Daniel Reijsbergen and Andrea Vandin. Transient and Steady-State Statistical Analysis for Discrete Event Simulators
Ludovic Henrio, Cosimo Laneve and Vincenzo Mastandrea. Analysis of synchronisation patterns in stateful active objects
Sven Linker. Spatial Reasoning about Motorway Traffic Safety with Isabelle/HOL
Joao F. Ferreira, Saul A. Johnson, Alexandra Mendes and Phillip J. Brooke. Certified Password Quality — A Case Study Using Coq and Linux Pluggable Authentication Modules
Pedro Ribeiro, Alvaro Miyazawa, Wei Li, Ana Cavalcanti and Jon Timmis. Modelling and Verification of Timed Robotic Controllers
Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl. Generalised Test Tables – a Practical Specification Language for Reactive Systems
Ajay Krishna, Pascal Poizat and Gwen Salaün. VBPMN: Automated Verification of BPMN Processes
Barbara Kordy and Wojciech Widel. How well can I secure my system?
Murat Moran and Dan Wallach. Verification of STAR-Vote and Evaluation of FDR and ProVerif
Dominic Steinhöfel and Nathan Wasser. A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch and Mattias Ulbrich. SemSlice: Exploiting Relational Verification for Automatic Program Slicing
Florian Frohn and Jürgen Giesl. Complexity Analysis for Java with AProVE
Hao Wu. MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams
Dalay Israel de Almeida Pereira, Marcel Vinicius Medeiros Oliveira, Madiel Conserva Filho and Sarah Raquel Da Rocha Silva. BTS: A Tool for Formal Component-based Development
Ferruccio Damiani, Michael Lienhardt, Radu Muschevici and Ina Schaefer. An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs
Stavros Aronis, Scott Fritchie and Kostis Sagonas. Testing and Verifying Chain Repair Methods for CORFU Using Stateless Model Checking
Wei Ji, Farn Wang and Peng Wu. Synthesizing Coalitions for Multi-Agent Games