Abstract is missing.
- Verified Compilation of Space-Efficient Reversible CircuitsMatthew Amy, Martin Roetteler, Krysta M. Svore. 3-21 [doi]
- Ascertaining Uncertainty for Efficient Exact Cache AnalysisValentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke. 22-40 [doi]
- Non-polynomial Worst-Case Analysis of Recursive ProgramsKrishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady. 41-63 [doi]
- Automated Resource Analysis with Coq Proof ObjectsQuentin Carbonneaux, Jan Hoffmann 0002, Thomas W. Reps, Zhong Shao. 64-85 [doi]
- Look for the Proof to Find the Program: Decorated-Component-Based Program SynthesisAdria Gascón, Ashish Tiwari, Brent Carmer, Umang Mathur. 86-103 [doi]
- E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal MethodsEshan Singh, Clark W. Barrett, Subhasish Mitra. 104-125 [doi]
- SMTCoq: A Plug-In for Integrating SMT Solvers into CoqBurak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett. 126-133 [doi]
- Efficient Parallel Strategy Improvement for Parity GamesJohn Fearnley. 137-154 [doi]
- Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown SystemsMarie Fortin, Anca Muscholl, Igor Walukiewicz. 155-175 [doi]
- Minimization of Symbolic TransducersOlli Saarikivi, Margus Veanes. 176-196 [doi]
- Abstract Interpretation with UnfoldingsMarcelo Sousa, César Rodríguez, Vijay D'Silva, Daniel Kroening. 197-216 [doi]
- Cutoff Bounds for Consensus AlgorithmsOgnjen Maric, Christoph Sprenger, David A. Basin. 217-237 [doi]
- Towards Verifying Nonlinear Integer ArithmeticPaul Beame, Vincent Liew. 238-258 [doi]
- Network-Wide Configuration SynthesisAhmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin T. Vechev. 261-281 [doi]
- Verifying Equivalence of Spark ProgramsShelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv. 282-300 [doi]
- Synchronization Synthesis for Network ProgramsJedidiah McClurg, Hossein Hojjat, Pavol Cerný. 301-321 [doi]
- BoSy: An Experimentation Framework for Bounded SynthesisPeter Faymonville, Bernd Finkbeiner, Leander Tentrup. 325-332 [doi]
- Bounded Synthesis for Streett, Rabin, and \text CTL^*Ayrat Khalimov, Roderick Bloem. 333-352 [doi]
- Quantitative Assume Guarantee SynthesisShaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner. 353-374 [doi]
- Syntax-Guided Optimal Synthesis for Chemical Reaction NetworksLuca Cardelli, Milan Ceska, Martin Fränzle, Marta Z. Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby. 375-395 [doi]
- Model Counting for Recursively-Defined StringsMinh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar. 399-418 [doi]
- A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMTSylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex. 419-435 [doi]
- A Correct-by-Decision Solution for Simultaneous Place and RouteAlexander Nadel. 436-452 [doi]
- Scaling Up DPLL(T) String Solvers Using Context-Dependent SimplificationAndrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli. 453-474 [doi]
- On Expansion and Resolution in CEGAR Based QBF SolvingLeander Tentrup. 475-494 [doi]
- A Decidable Fragment in Separation Logic with Inductive Predicates and ArithmeticQuang Loc Le, Makoto Tatsuta, Jun Sun 0001, Wei-Ngan Chin. 495-517 [doi]
- Finding Fix Locations for CFL-Reachability Analyses via Minimum CutsAndrei Marian Dan, Manu Sridharan, Satish Chandra 0001, Jean-Baptiste Jeannin, Martin T. Vechev. 521-541 [doi]
- Proving Linearizability Using Forward SimulationsAhmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil. 542-563 [doi]
- EAHyper: Satisfiability, Implication, and Equivalence Checking of HyperpropertiesBernd Finkbeiner, Christopher Hahn, Marvin Stenger. 564-570 [doi]
- Automating Induction for Solving Horn ClausesHiroshi Unno, Sho Torii, Hiroki Sakamoto. 571-591 [doi]
- A Storm is Coming: A Modern Probabilistic Model CheckerChristian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk 0001. 592-600 [doi]
- On Multiphase-Linear Ranking FunctionsAmir M. Ben-Amram, Samir Genaim. 601-620 [doi]