Abstract is missing.
- Poling: SMT Aided Linearizability ProofsHe Zhu, Gustavo Petri, Suresh Jagannathan. 3-19 [doi]
- Finding Bounded Path in Graph Using SMT for Automatic Clock RoutingAmit Erez, Alexander Nadel. 20-36 [doi]
- Cutting the MixJürgen Christ, Jochen Hoenicke. 37-52 [doi]
- The Inez Mathematical Programming Modulo Theories FrameworkPanagiotis Manolios, Jorge Pais, Vasilis Papavasileiou. 53-69 [doi]
- Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable SetsFahiem Bacchus, George Katsirelos. 70-86 [doi]
- Deciding Local Theory Extensions via E-matchingKshitij Bansal, Andrew Reynolds, Tim King 0001, Clark W. Barrett, Thomas Wies. 87-105 [doi]
- Modular Deductive Verification of Multiprocessor Hardware DesignsMuralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave. 109-127 [doi]
- Word-Level Symbolic Trajectory EvaluationSupratik Chakraborty, Zurab Khasidashvili, Carl-Johan H. Seger, Rajkumar Gajavelly, Tanmay Haldankar, Dinesh Chhatani, Rakesh Mistry. 128-143 [doi]
- Verifying Linearizability of Intel® Software Guard ExtensionsRebekah Leslie-Hurd, Dror Caspi, Matthew Fernandez. 144-160 [doi]
- Synthesis Through UnificationRajeev Alur, Pavol Cerný, Arjun Radhakrishna. 163-179 [doi]
- From Non-preemptive to Preemptive Scheduling Using Synchronization SynthesisPavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach. 180-197 [doi]
- Counterexample-Guided Quantifier Instantiation for Synthesis in SMTAndrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett. 198-216 [doi]
- Deductive Program RepairEtienne Kneuss, Manos Koukoutos, Viktor Kuncak. 217-233 [doi]
- Quantifying Conformance Using the Skorokhod MetricJyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu. 234-250 [doi]
- Pareto Curves of Multidimensional Mean-Payoff GamesRomain Brenguier, Jean-François Raskin. 251-267 [doi]
- Conflict-Driven Conditional TerminationVijay D'Silva, Caterina Urban. 271-286 [doi]
- Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional ProgramsTakuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi 0001. 287-303 [doi]
- Complexity of Bradley-Manna-Sipma Lexicographic Ranking FunctionsAmir M. Ben-Amram, Samir Genaim. 304-321 [doi]
- Measuring with Timed PatternsThomas Ferrère, Oded Maler, Dejan Nickovic, Dogan Ulus. 322-337 [doi]
- Automatic Verification of Stability and Safety for Delay Differential EquationsLiang Zou, Martin Fränzle, Naijun Zhan, Peter Nazier Mosaad. 338-355 [doi]
- Time Robustness in MTL and Expressivity in Hybrid System FalsificationTakumi Akazaki, Ichiro Hasuo. 356-374 [doi]
- Adaptive Concretization for Parallel Program SynthesisJinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, Jeffrey S. Foster. 377-394 [doi]
- Automatic Completion of Distributed Protocols with SymmetryRajeev Alur, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, Abhishek Udupa. 395-412 [doi]
- An Axiomatic Specification for Sequential Memory ModelsWilliam Mansky, Dmitri Garbuzov, Steve Zdancewic. 413-428 [doi]
- Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous SystemsAnkush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, John C. Eidson. 429-448 [doi]
- Automated and Modular Refinement Reasoning for Concurrent ProgramsChris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran. 449-465 [doi]