default search action
27th CAV 2015: San Francisco, CA, USA
- Daniel Kroening, Corina S. Pasareanu:
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. Lecture Notes in Computer Science 9207, Springer 2015, ISBN 978-3-319-21667-6
SMT Techniques and Applications
- He Zhu, Gustavo Petri, Suresh Jagannathan:
Poling: SMT Aided Linearizability Proofs. 3-19 - Amit Erez, Alexander Nadel:
Finding Bounded Path in Graph Using SMT for Automatic Clock Routing. 20-36 - Jürgen Christ, Jochen Hoenicke:
Cutting the Mix. 37-52 - Panagiotis Manolios, Jorge Pais, Vasilis Papavasileiou:
The Inez Mathematical Programming Modulo Theories Framework. 53-69 - Fahiem Bacchus, George Katsirelos:
Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets. 70-86 - Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
Deciding Local Theory Extensions via E-matching. 87-105
HW Verification
- Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave:
Modular Deductive Verification of Multiprocessor Hardware Designs. 109-127 - Supratik Chakraborty, Zurab Khasidashvili, Carl-Johan H. Seger, Rajkumar Gajavelly, Tanmay Haldankar, Dinesh Chhatani, Rakesh Mistry:
Word-Level Symbolic Trajectory Evaluation. 128-143 - Rebekah Leslie-Hurd, Dror Caspi, Matthew Fernandez:
Verifying Linearizability of Intel® Software Guard Extensions. 144-160
Synthesis
- Rajeev Alur, Pavol Cerný, Arjun Radhakrishna:
Synthesis Through Unification. 163-179 - Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach:
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. 180-197 - Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. 198-216 - Etienne Kneuss, Manos Koukoutos, Viktor Kuncak:
Deductive Program Repair. 217-233 - Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu:
Quantifying Conformance Using the Skorokhod Metric. 234-250 - Romain Brenguier, Jean-François Raskin:
Pareto Curves of Multidimensional Mean-Payoff Games. 251-267
Termination
- Vijay D'Silva, Caterina Urban:
Conflict-Driven Conditional Termination. 271-286 - Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi:
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. 287-303 - Amir M. Ben-Amram, Samir Genaim:
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. 304-321 - Thomas Ferrère, Oded Maler, Dejan Nickovic, Dogan Ulus:
Measuring with Timed Patterns. 322-337 - Liang Zou, Martin Fränzle, Naijun Zhan, Peter Nazier Mosaad:
Automatic Verification of Stability and Safety for Delay Differential Equations. 338-355 - Takumi Akazaki, Ichiro Hasuo:
Time Robustness in MTL and Expressivity in Hybrid System Falsification. 356-374
Concurrency
- Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, Jeffrey S. Foster:
Adaptive Concretization for Parallel Program Synthesis. 377-394 - Rajeev Alur, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, Abhishek Udupa:
Automatic Completion of Distributed Protocols with Symmetry. 395-412 - William Mansky, Dmitri Garbuzov, Steve Zdancewic:
An Axiomatic Specification for Sequential Memory Models. 413-428 - Ankush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, John C. Eidson:
Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems. 429-448 - Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran:
Automated and Modular Refinement Reasoning for Concurrent Programs. 449-465
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.