Abstract is missing.
- On the Semantics of Snapshot IsolationAzalea Raad, Ori Lahav, Viktor Vafeiadis. 1-23 [doi]
- Program Synthesis with Equivalence ReductionCalvin Smith, Aws Albarghouthi. 24-47 [doi]
- Minimal Synthesis of String to String Functions from ExamplesJad Hamza, Viktor Kuncak. 48-69 [doi]
- Automatic Program Repair Using Formal Verification and Expression TemplatesThanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin. 70-91 [doi]
- Lazy but Effective Functional SynthesisGrigory Fedyukovich, Arie Gurfinkel, Aarti Gupta. 92-113 [doi]
- Static Analysis of Binary Code with Memory Indirections Using PolyhedraClément Ballabriga, Julien Forget, Laure Gonnord, Giuseppe Lipari, Jordy Ruiz. 114-135 [doi]
- Disjunctive Relational Abstract Interpretation for Interprocedural Program AnalysisRémy Boutonnet, Nicolas Halbwachs. 136-159 [doi]
- Exploiting Pointer Analysis in Memory Models for Deductive VerificationQuentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski. 160-182 [doi]
- Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded ProgramsAnja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard. 183-204 [doi]
- Relatively Complete Pushdown Analysis of Escape ContinuationsKimball Germane, Matthew Might. 205-225 [doi]
- Demand Control-Flow AnalysisKimball Germane, Jay McCarthy, Michael D. Adams 0001, Matthew Might. 226-246 [doi]
- Effect-Driven Flow AnalysisJens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover. 247-274 [doi]
- Type-Directed Bounding of Collections in Reactive ProgramsTianhan Lu, Pavol Cerný, Bor-Yuh Evan Chang, Ashutosh Trivedi 0001. 275-296 [doi]
- Solving and Interpolating Constant Arrays Based on Weak EquivalencesJochen Hoenicke, Tanja Schindler. 297-317 [doi]
- A Decidable Logic for Tree Data-Structures with MeasurementsXiaokang Qiu, Yanjun Wang. 318-341 [doi]
- A Practical Algorithm for Structure EmbeddingCharlie Murphy, Zachary Kincaid. 342-362 [doi]
- euforia: Complete Software Model Checking with Uninterpreted FunctionsDenis Bueno, Karem A. Sakallah. 363-385 [doi]
- Fast BGP Simulation of Large DatacentersNuno P. Lopes, Andrey Rybalchenko. 386-408 [doi]
- Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model CheckingÉtienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat. 409-424 [doi]
- Application of Abstract Interpretation to the Automotive Electronic Control SystemTomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura. 425-445 [doi]
- Syntactic Partial Order Compression for Probabilistic ReachabilityGereon Fox, Daniel Stan, Holger Hermanns. 446-467 [doi]
- Termination of Nondeterministic Probabilistic ProgramsHongfei Fu, Krishnendu Chatterjee. 468-490 [doi]
- Parametric Timed Broadcast ProtocolsÉtienne André, Benoît Delahaye, Paulin Fournier, Didier Lime. 491-512 [doi]
- Flat Model Checking for Counting LTL Using Quantifier-Free Presburger ArithmeticNormann Decker, Anton Pirogov. 513-534 [doi]
- A Parallel Relation-Based Algorithm for Symbolic Bisimulation MinimizationRichard Huybers, Alfons Laarman. 535-554 [doi]
- Combining Refinement of Parametric Models with Goal-Oriented Reduction of DynamicsStefan Haar, Juraj Kolcák, Loïc Paulevé. 555-576 [doi]
- Mechanically Proving Determinacy of Hierarchical Block Diagram TranslationsViorel Preoteasa, Iulia Dragomir, Stavros Tripakis. 577-600 [doi]