Abstract is missing.
- Model Checking at Scale: Automated Air Traffic Control Design Space ExplorationMarco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier. 3-22 [doi]
- Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable CheckersStuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky. 23-41 [doi]
- End-to-End Verification of Processors with ISA-FormalAlastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, Ali Zaidi. 42-58 [doi]
- A Practical Verification Framework for Preemptive OS KernelsFengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, Zhaohui Li. 59-79 [doi]
- Probabilistic Automated Language Learning for Configuration FilesMark Santolucito, Ennan Zhai, Ruzica Piskac. 80-87 [doi]
- The Commutativity Problem of the MapReduce Framework: A Transducer-Based ApproachYu-Fang Chen, Lei Song, Zhilin Wu. 91-111 [doi]
- Liveness of Randomised Parameterised Systems under Arbitrary SchedulersAnthony W. Lin, Philipp Rümmer. 112-133 [doi]
- Stateless Model Checking for POWERParosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson. 134-156 [doi]
- Hitting Families of Schedules for Asynchronous ProgramsDmitry Chistikov, Rupak Majumdar, Filip Niksic. 157-176 [doi]
- ParCoSS: Efficient Parallelized Compiled Symbolic SimulationVladimir Herdt, Hoang M. Le, Daniel Große, Rolf Drechsler. 177-183 [doi]
- XSat: A Fast Floating-Point Satisfiability SolverZhoulai Fu, Zhendong Su. 187-209 [doi]
- Effectively Propositional InterpolantsSamuel Drews, Aws Albarghouthi. 210-229 [doi]
- Array Folds LogicPrzemyslaw Daca, Thomas A. Henzinger, Andrey Kupriyanov. 230-248 [doi]
- Compositional Synthesis of Reactive Controllers for Multi-agent SystemsRajeev Alur, Salar Moarref, Ufuk Topcu. 251-269 [doi]
- Solving Parity Games via Priority PromotionMassimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero. 270-290 [doi]
- A Simple Algorithm for Solving Qualitative Probabilistic Parity GamesErnst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang. 291-311 [doi]
- Limit-Deterministic Büchi Automata for Linear Temporal LogicSalomon Sickert, Javier Esparza, Stefan Jaax, Jan Kretínský. 312-332 [doi]
- Slugs: Extensible GR(1) SynthesisRüdiger Ehlers, Vasumathi Raman. 333-339 [doi]
- Synthesis of Fault-Attack Countermeasures for Cryptographic CircuitsHassan Eldib, Meng Wu, Chao Wang. 343-363 [doi]
- A SAT-Based Counterexample Guided Method for Unbounded SynthesisAlexander Legg, Nina Narodytska, Leonid Ryzhyk. 364-382 [doi]
- Qlose: Program Repair with Quantitative ObjectivesLoris D'Antoni, Roopsha Samanta, Rishabh Singh. 383-401 [doi]
- BDD-Based Boolean Functional SynthesisDror Fried, Lucas M. Tabajara, Moshe Y. Vardi. 402-421 [doi]
- Soufflé: On Synthesis of Program AnalyzersHerbert Jordan, Bernhard Scholz, Pavle Subotic. 422-430 [doi]
- Property Directed Equivalence via Abstract SimulationGrigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina. 433-453 [doi]
- Combining Model Learning and Model Checking to Analyze TCP ImplementationsPaul Fiterau-Brostean, Ramon Janssen, Frits W. Vaandrager. 454-471 [doi]
- BFS-Based Model Checking of Linear-Time Properties with an Application on GPUsAnton Wijs. 472-493 [doi]
- BigraphER: Rewriting and Analysis Engine for BigraphsMichele Sevegnani, Muffy Calder. 494-501 [doi]
- Verification-Aided Debugging: An Interactive Web-Service for Exploring Error WitnessesDirk Beyer 0001, Matthias Dangl. 502-509 [doi]
- The Kind 2 Model CheckerAdrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli. 510-517 [doi]