Abstract is missing.
- Model Integration and Cyber Physical Systems: A Semantics PerspectiveJanos Sztipanovits. 1 [doi]
- Some Thoughts on Behavioral ProgrammingDavid Harel. 2 [doi]
- The Only Way Is UpJasmin Fisher, Nir Piterman, Moshe Y. Vardi. 3-11 [doi]
- Does It Pay to Extend the Perimeter of a World Model?Werner Damm, Bernd Finkbeiner. 12-26 [doi]
- System Verification through Program VerificationDaniel Dietsch, Bernd Westphal, Andreas Podelski. 27-41 [doi]
- Adaptive Cruise Control: Hybrid, Distributed, and Now Formally VerifiedSarah M. Loos, André Platzer, Ligia Nistor. 42-56 [doi]
- TraceContract: A Scala DSL for Trace AnalysisHoward Barringer, Klaus Havelund. 57-72 [doi]
- Using Debuggers to Understand Failed Verification AttemptsPeter Müller, Joseph N. Ruskiewicz. 73-87 [doi]
- Sampling-Based Runtime VerificationBorzoo Bonakdarpour, Samaneh Navabpour, Sebastian Fischmeister. 88-102 [doi]
- Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADPFabienne Boyer, Olivier Gruber, Gwen Salaün. 103-117 [doi]
- Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking SystemsAnne Elisabeth Haxthausen, Andreas A. Kjær, Marie Le Bliguet. 118-132 [doi]
- Relational Reasoning via SMT SolvingAboubakr Achraf El Ghazi, Mana Taghdiri. 133-148 [doi]
- Building VCL Models and Automatically Generating Z Specifications from ThemNuno Amálio, Christian Glodt, Pierre Kelsen. 149-153 [doi]
- The 1st Verified Software Competition: Experience ReportVladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß. 154-168 [doi]
- Validated Compilation through LogicGuodong Li. 169-183 [doi]
- Certification of Safe Polynomial Memory BoundsJavier de Dios, Ricardo Peña. 184-199 [doi]
- Relational Verification Using Product ProgramsGilles Barthe, Juan Manuel Crespo, César Kunz. 200-214 [doi]
- Specifying Confidentiality in CircusMichael J. Banks, Jeremy L. Jacob. 215-230 [doi]
- Formally Verifying Isolation and Availability in an Idealized Model of VirtualizationGilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna. 231-245 [doi]
- The Safety-Critical Java Memory Model: A Formal AccountAna Cavalcanti, Andy J. Wellings, Jim Woodcock. 246-261 [doi]
- Failure-Divergence Refinement of Compensating Communicating ProcessesZhenbang Chen, Zhiming Liu, Ji Wang. 262-277 [doi]
- Termination without /checkmark/checkmark in CSPSteve Dunne. 278-292 [doi]
- Timed Migration and Interaction with Access PermissionsGabriel Ciobanu, Maciej Koutny. 293-307 [doi]
- From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods CommunityJonathan P. Bowen, Steve Reeves. 308-322 [doi]
- Verifying Linearisability with Potential Linearisation PointsJohn Derrick, Gerhard Schellhorn, Heike Wehrheim. 323-337 [doi]
- Refinement-Based Verification of Local Synchronization AlgorithmsDominique Méry, Mohamed Mosbah, Mohamed Tounsi. 338-352 [doi]
- Simulating Concurrent Behaviors with Worst-Case Cost BoundsElvira Albert, Samir Genaim, Miguel Gómez-Zamalloa, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa. 353-368 [doi]
- Automatically Refining Partial Specifications for Program VerificationShengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He. 369-385 [doi]
- Structured Specifications for Better Verification of Heap-Manipulating ProgramsCristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin. 386-401 [doi]
- Verification of Unloadable ModulesBart Jacobs, Jan Smans, Frank Piessens. 402-416 [doi]
- A Multi-encoding Approach for LTL Symbolic Satisfiability CheckingKristin Y. Rozier, Moshe Y. Vardi. 417-431 [doi]
- On Combining State Space Reductions with Global Fairness AssumptionsShao Jie Zhang, Jun Sun 0001, Jun Pang, Yang Liu 0003, Jin Song Dong. 432-447 [doi]