دانلود کتاب Computer Aided Verification : 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I

فهرست مطالب :

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