Abstract is missing.
- The Human in Formal MethodsShriram Krishnamurthi, Tim Nelson. 3-10 [doi]
- Successes in Deployed Verified Software (and Insights on Key Social Factors)June Andronick. 11-17 [doi]
- Provably Correct Floating-Point Implementation of a Point-in-Polygon AlgorithmMariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz. 21-37 [doi]
- Formally Verified Roundoff Errors Using SMT-based Certificates and SubdivisionsJoachim Bard, Heiko Becker, Eva Darulova. 38-44 [doi]
- Mechanically Verifying the Fundamental Liveness Property of the Chord ProtocolJean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali. 45-63 [doi]
- On the Nature of Symbolic ExecutionFrank S. de Boer, Marcello M. Bonsangue. 64-80 [doi]
- GR(1)*: GR(1) Specifications Extended with Existential GuaranteesGal Amram, Shahar Maoz, Or Pistiner. 83-100 [doi]
- Counterexample-Driven Synthesis for Probabilistic Program SketchesMilan Ceska, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. 101-120 [doi]
- Synthesis of Railway Signaling Layout from Local Capacity SpecificationsBjørnar Luteberget, Christian Johansen, Martin Steffen. 121-137 [doi]
- Pegasus: A Framework for Sound Continuous Invariant GenerationAndrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer. 138-157 [doi]
- A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive SystemsYongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu 0003. 161-178 [doi]
- Verifying Correctness of Persistent Concurrent Data StructuresJohn Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim. 179-195 [doi]
- Compositional Verification of Concurrent Systems by Combining BisimulationsFrédéric Lang, Radu Mateescu 0001, Franco Mazzanti. 196-213 [doi]
- Towards a Model-Checker for CircusArtur Oliveira Gomes, Andrew Butterfield. 217-234 [doi]
- Circus2CSP: A Tool for Model-Checking Circus Using FDRArtur Oliveira Gomes, Andrew Butterfield. 235-242 [doi]
- How Hard Is Finding Shortest Counter-Example Lassos in Model Checking?Rüdiger Ehlers. 245-261 [doi]
- From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating AutomataSimon Jantsch, David Müller 0001, Christel Baier, Joachim Klein 0001. 262-279 [doi]
- Generic Partition Refinement and Weighted Tree AutomataHans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann. 280-297 [doi]
- Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic GamesMarta Kwiatkowska, Gethin Norman, David Parker 0001, Gabriel Santos. 298-315 [doi]
- Abstract ExecutionDominic Steinhöfel, Reiner Hähnle. 319-336 [doi]
- Static Analysis for Detecting High-Level Races in RTOS KernelsAbhishek Singh, Rekha Pai, Deepak D'Souza, Meenakshi D'Souza. 337-353 [doi]
- Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic LogicSimon Lunel, Stefan Mitsch, Benoît Boyer, Jean-Pierre Talpin. 354-370 [doi]
- An Axiomatic Approach to Liveness for Differential EquationsYong Kiam Tan, André Platzer. 371-388 [doi]
- Local Consistency Check in Synchronous Dataflow ModelsDina Irofti, Paul Dubrulle. 389-405 [doi]
- Gray-Box Monitoring of HyperpropertiesSandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour. 406-424 [doi]
- Quantitative Verification of Numerical Stability for Kalman FiltersAlexandros Evangelidis, David Parker 0001. 425-441 [doi]
- Concolic Testing Heap-Manipulating ProgramsLong H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun 0001. 442-461 [doi]
- Formal Semantics Extraction from Natural Language Specifications for ARMAnh V. Vu, Mizuhito Ogawa. 465-483 [doi]
- GOSPEL - Providing OCaml with a Formal Specification LanguageArthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira. 484-501 [doi]
- Unification in Matching LogicAndrei Arusoaie, Dorel Lucanu. 502-518 [doi]
- Embedding High-Level Formal Specifications into ApplicationsPhilipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel. 519-535 [doi]
- Value-Dependent Information-Flow Security on Weak Memory ModelsGraeme Smith, Nicholas Coughlin, Toby Murray. 539-555 [doi]
- Reasoning Formally About Database Queries and UpdatesJon Haël Brenas, Rachid Echahed, Martin Strecker. 556-572 [doi]
- Abstraction and Subsumption in Modular Verification of C ProgramsLennart Beringer, Andrew W. Appel. 573-590 [doi]
- IELE: A Rigorously Designed Language and Tool Ecosystem for the BlockchainTheodoros Kasampalis, Dwight Guth, Brandon M. Moore, Traian-Florin Serbanuta, Yi Zhang, Daniele Filaretti, Virgil Nicolae Serbanuta, Ralph Johnson, Grigore Rosu. 593-610 [doi]
- APML: An Architecture Proof Modeling LanguageDiego Marmsoler, Genc Blakqori. 611-630 [doi]
- Learning Deterministic Variable Automata over Infinite AlphabetsSarai Sheinvald. 633-650 [doi]
- L^* L ∗ -Based Learning of Markov Decision ProcessesMartin Tappler, Bernhard K. Aichernig, Giovanni Bacci 0001, Maria Eichlseder, Kim G. Larsen. 651-669 [doi]
- Star-Based Reachability Analysis of Deep Neural NetworksHoang-Dung Tran, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Taylor T. Johnson. 670-686 [doi]
- SOA and the Button ProblemSung-Shik Jongmans, Arjan Lamers, Marko C. J. D. van Eekelen. 689-706 [doi]
- Controlling Large Boolean Networks with Temporary and Permanent PerturbationsCui Su, Soumya Paul, Jun Pang 0001. 707-724 [doi]
- Formal Methods Applicability on Space Applications Specification and Implementation Using MORA-TSPDaniel Silveira, Andreas Jung, Marcel Verhoef, Tiago Jorge. 727-737 [doi]
- Industrial Application of Event-B to a Wayside Train Monitoring System: Formal Conceptual Data AnalysisRobert Eschbach. 738-745 [doi]
- Property-Driven Software Analysis - (Extended Abstract)Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez. 746-750 [doi]
- Practical Application of SPARK to OpenUxASM. Anthony Aiello, Claire Dross, Patrick Rogers, Laura Humphrey, James Hamil. 751-761 [doi]
- Adopting Formal Methods in an Industrial Setting: The Railways CaseMaurice H. ter Beek, Arne Borälv, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Christer Löfving, Franco Mazzanti. 762-772 [doi]