default search action
29th CAV 2017: Heidelberg, Germany
- Rupak Majumdar, Viktor Kuncak:
Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science 10426, Springer 2017, ISBN 978-3-319-63386-2
Invited Contributions
- Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu:
Safety Verification of Deep Neural Networks. 3-29 - Viktor Vafeiadis:
Program Verification Under Weak Memory Consistency Using Separation Logic. 30-46 - Loris D'Antoni, Margus Veanes:
The Power of Symbolic Automata and Transducers. 47-67 - Xujie Si, Xin Zhang, Radu Grigore, Mayur Naik:
Maximum Satisfiability in Software Analysis: Applications and Techniques. 68-94
Probabilistic Systems
- Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer:
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. 97-117 - Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar:
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. 118-139 - Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen:
Markov Automata with Multiple Objectives. 140-159 - Christel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich:
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. 160-180 - Aws Albarghouthi, Loris D'Antoni, Samuel Drews:
Repairing Decision-Making Programs Under Uncertainty. 181-200 - Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer:
Value Iteration for Long-Run Average Reward in Markov Decision Processes. 201-221
Data Driven Techniques
- Hendrik Roehm, Thomas Heinz, Eva Charlotte Mayer:
STLInspector: STL Validation with Guarantees. 225-232 - Pavol Bielik, Veselin Raychev, Martin T. Vechev:
Learning a Static Analyzer from Data. 233-253 - Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav:
Synthesis with Abstract Examples. 254-278 - Sarah E. Chasins, Phitchaya Mangpo Phothilimthana:
Data-Driven Synthesis of Full Probabilistic Programs. 279-304 - Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia:
Logical Clustering and Learning for Time-Series Data. 305-325
Runtime Verification
- Dogan Ulus:
Montre: A Tool for Monitoring Timed Regular Expressions. 329-335 - Konstantin Selyunin, Stefan Jaksic, Thang Nguyen, Christian Reidl, Udo Hafner, Ezio Bartocci, Dejan Nickovic, Radu Grosu:
Runtime Monitoring with Recovery of the SENT Communication Protocol. 336-355 - David A. Basin, Felix Klaedtke, Eugen Zalinescu:
Runtime Verification of Temporal Properties over Out-of-Order Data Streams. 356-376
Cyber-Physical Systems
- Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul L. Jones, Scott A. Smolka, Radu Grosu:
Lagrangian Reachabililty. 379-400 - Stanley Bak, Parasara Sridhar Duggirala:
Simulation-Equivalent Reachability of Large Linear Systems with Inputs. 401-420 - Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege:
MightyL: A Compositional Translation from MITL to Timed Automata. 421-440 - Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan:
DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems. 441-461 - Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen:
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. 462-482 - Arvind S. Adimoolam, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin:
Classification and Coverage-Based Falsification for Embedded Control Systems. 483-503
Concurrency
- Rajeev Alur, Joseph Devietti, Omar S. Navarro Leija, Nimit Singhania:
GPUDrano: Detecting Uncoalesced Accesses in GPU Programs. 507-525 - Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Peter J. Stuckey:
Context-Sensitive Dynamic Partial Order Reduction. 526-543 - Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson:
Starling: Lightweight Concurrency Verification with Views. 544-569 - Anton Wijs, Thomas Neele:
Compositional Model Checking with Incremental Counter-Example Construction. 570-590 - Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek:
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems. 591-598
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.