Abstract is missing.
- Synthesis and Some of Its ChallengesWolfgang Thomas. 1 [doi]
- Model Checking Cell BiologyDavid L. Dill. 2 [doi]
- Synthesizing Programs with Constraint SolversRastislav Bodík, Emina Torlak. 3 [doi]
- IC3 and beyond: Incremental, Inductive VerificationAaron R. Bradley. 4 [doi]
- Formal Verification of Genetic CircuitsChris J. Myers. 5 [doi]
- From C to Infinity and Back: Unbounded Auto-active Verification with VCCMichal Moskal. 6 [doi]
- Deterministic Automata for the (F, G)-Fragment of LTLJan Kretínský, Javier Esparza. 7-22 [doi]
- Efficient Controller Synthesis for Consumption Games with Multiple Resource TypesTomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný. 23-38 [doi]
- ACTL ∩ LTL SynthesisRüdiger Ehlers. 39-54 [doi]
- Learning Boolean Functions IncrementallyYu-Fang Chen, Bow-Yaw Wang. 55-70 [doi]
- Interpolants as ClassifiersRahul Sharma 0001, Aditya V. Nori, Alex Aiken. 71-87 [doi]
- Termination Analysis with Algorithmic LearningWonchan Lee, Bow-Yaw Wang, Kwangkeun Yi. 88-104 [doi]
- Automated Termination Proofs for Java Programs with Cyclic DataMarc Brockschmidt, Richard Musiol, Carsten Otto, Jürgen Giesl. 105-122 [doi]
- Proving Termination of Probabilistic Programs Using PatternsJavier Esparza, Andreas Gaiser, Stefan Kiefer. 123-138 [doi]
- The Gauge Domain: Scalable Analysis of Linear Inequality InvariantsArnaud Venet. 139-154 [doi]
- Diagnosing Abstraction Failure for Separation Logic-Based AnalysesJosh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger. 155-173 [doi]
- A Method for Symbolic Computation of Abstract OperationsAditya V. Thakur, Thomas W. Reps. 174-192 [doi]
- Leveraging Interpolant Strength in Model CheckingSimone Fulvio Rollini, Ondrej Sery, Natasha Sharygina. 193-209 [doi]
- Detecting Fair Non-termination in Multithreaded ProgramsMohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal. 210-226 [doi]
- Lock Removal for Concurrent Trace ProgramsVineet Kahlon, Chao Wang. 227-242 [doi]
- How to Prove Algorithms LinearisableGerhard Schellhorn, Heike Wehrheim, John Derrick. 243-259 [doi]
- Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with CountersMatthew Hague, Anthony Widjaja Lin. 260-276 [doi]
- Software Model Checking via IC3Alessandro Cimatti, Alberto Griggio. 277-293 [doi]
- Delayed Continuous-Time Markov Chains for Genetic Regulatory CircuitsCalin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu, Ali Sezgin. 294-309 [doi]
- Assume-Guarantee Abstraction Refinement for Probabilistic SystemsAnvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke. 310-326 [doi]
- Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model CheckingCyrille Jégourel, Axel Legay, Sean Sedwards. 327-342 [doi]
- Timed Relational Abstractions for Sampled Data Control SystemsAditya Zutshi, Sriram Sankaranarayanan, Ashish Tiwari. 343-361 [doi]
- Approximately Bisimilar Symbolic Models for Digital Control SystemsRupak Majumdar, Majid Zamani. 362-377 [doi]
- Formal Verification and Validation of ERTMS Industrial Railway Train Spacing SystemAlessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero, Andrei Tchaltsev. 378-393 [doi]
- Minimum Satisfying Assignments for SMTIsil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken. 394-409 [doi]
- When Boolean Satisfiability Meets Gaussian Elimination in a Simplex WayCheng-Shen Han, Jie-Hong Roland Jiang. 410-426 [doi]
- A Solver for Reachability Modulo TheoriesAkash Lal, Shaz Qadeer, Shuvendu K. Lahiri. 427-443 [doi]
- On Decidability of Prebisimulation for Timed AutomataShibashis Guha, Chinmay Narayan, S. Arun-Kumar. 444-461 [doi]
- Exercises in Nonstandard Static Analysis of Hybrid SystemsIchiro Hasuo, Kohei Suenaga. 462-478 [doi]
- A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceExSergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle. 479-494 [doi]
- An Axiomatic Memory Model for POWER MultiprocessorsSela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams. 495-512 [doi]
- nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug TracesFlavio M. de Paula, Alan J. Hu, Amir Nahir. 513-531 [doi]
- Incremental, Inductive CTL Model CheckingZyad Hassan, Aaron R. Bradley, Fabio Somenzi. 532-547 [doi]
- Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction RefinementMatthew Fredrikson, Richard Joiner, Somesh Jha, Thomas W. Reps, Phillip A. Porras, Hassen Saïdi, Vinod Yegneswaran. 548-563 [doi]
- Automatic Quantification of Cache Side-ChannelsBoris Köpf, Laurent Mauborgne, Martín Ochoa. 564-580 [doi]
- Secure Programming via Visibly Pushdown Safety GamesWilliam R. Harris, Somesh Jha, Thomas W. Reps. 581-598 [doi]
- Alternate and Learn: Finding Witnesses without Looking All overNishant Sinha, Nimit Singhania, Satish Chandra, Manu Sridharan. 599-615 [doi]
- A Complete Method for Symmetry Reduction in Safety VerificationDuc-Hiep Chu, Joxan Jaffar. 616-633 [doi]
- Synthesizing Number Transformations from Input-Output ExamplesRishabh Singh, Sumit Gulwani. 634-651 [doi]
- Acacia+, a Tool for LTL SynthesisAaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, Jean-François Raskin. 652-657 [doi]
- MGSyn: Automatic Synthesis for Industrial AutomationChih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl, Alois Knoll. 658-664 [doi]
- OpenNWA: A Nested-Word Automaton LibraryEvan Driscoll, Aditya V. Thakur, Thomas W. Reps. 665-671 [doi]
- Ufo: A Framework for Abstraction- and Interpolation-Based Software VerificationAws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik. 672-678 [doi]
- SAFARI: SMT-Based Abstraction for Arrays with InterpolantsFrancesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina. 679-685 [doi]
- Bma: Visual Tool for Modeling and Analyzing Biological NetworksDavid Benque, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex S. Taylor, Moshe Y. Vardi. 686-692 [doi]
- APEX: An Analyzer for Open Probabilistic ProgramsStefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. 693-698 [doi]
- Recent Developments in FDRPhilip J. Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell. 699-704 [doi]
- A Model Checker for Hierarchical Probabilistic Real-Time SystemsSongzheng Song, Jun Sun 0001, Yang Liu 0003, Jin Song Dong. 705-711 [doi]
- SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative ProgramsShuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo. 712-717 [doi]
- Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool PaperSylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi. 718-724 [doi]
- HybridSAL Relational AbstracterAshish Tiwari. 725-731 [doi]
- Euler: A System for Numerical Optimization of ProgramsSwarat Chaudhuri, Armando Solar-Lezama. 732-737 [doi]
- SPT: Storyboard Programming ToolRishabh Singh, Armando Solar-Lezama. 738-743 [doi]
- CSolve: Verifying C with Liquid TypesPatrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala. 744-750 [doi]
- passert: A Tool for Debugging Parallel ProgramsDaniel Schwartz-Narbonne, Feng Liu, David I. August, Sharad Malik. 751-757 [doi]
- TRACER: A Symbolic Execution Tool for VerificationJoxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa. 758-766 [doi]
- Joogie: Infeasible Code Detection for JavaStephan Arlt, Martin Schäf. 767-773 [doi]
- Hector: An Equivalence Checker for a Higher-Order Fragment of MLDavid Hopkins, Andrzej S. Murawski, C.-H. Luke Ong. 774-780 [doi]
- Resource Aware MLJan Hoffmann 0002, Klaus Aehlig, Martin Hofmann. 781-786 [doi]