| Description |
1 online resource (xvi, 789 pages) : illustrations |
| Series |
Lecture notes in computer science, 1611-3349 ; 7358 |
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
|
Lecture notes in computer science ; 7358. 1611-3349
|
|
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
|
| Contents |
Synthesis and Some of Its Challenges / Wolfgang Thomas -- Model Checking Cell Biology / David L. Dill -- Synthesizing Programs with Constraint Solvers / Rastislav Bodik and Emina Torlak -- IC3 and beyond: Incremental, Inductive Verification / Aaron R. Bradley -- Formal Verification of Genetic Circuits / Chris J. Myers -- From C to Infinity and Back: Unbounded Auto-active Verification with VCC / Michał Moskal -- Deterministic Automata for the (F, G)-Fragment of LTL / Jan Křetínský and Javier Esparza -- Efficient Controller Synthesis for Consumption Games with Multiple Resource Types / Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera and Petr Novotný -- ACTL [inverted U] LTL Synthesis / Rüdiger Ehlers -- Learning Boolean Functions Incrementally / Yu-Fang Chen and Bow-Yaw Wang -- Interpolants as Classifiers / Rahul Sharma, Aditya V. Nori and Alex Aiken -- Termination Analysis with Algorithmic Learning / Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi -- Automated Termination Proofs for Java Programs with Cyclic Data / Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl -- Proving Termination of Probabilistic Programs Using Patterns / Javier Esparza, Andreas Gaiser and Stefan Kiefer -- The Gauge Domain: Scalable Analysis of Linear Inequality Invariants / Arnaud J. Venet -- Diagnosing Abstraction Failure for Separation Logic-Based Analyses / Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph M. Wintersteiger |
|
A Method for Symbolic Computation of Abstract Operations / Aditya Thakur and Thomas Reps -- Leveraging Interpolant Strength in Model Checking / Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina -- Detecting Fair Non-termination in Multithreaded Programs / Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal -- Lock Removal for Concurrent Trace Programs / Vineet Kahlon and Chao Wang -- How to Prove Algorithms Linearisable / Gerhard Schellhorn, Heike Wehrheim and John Derrick -- Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters / Matthew Hague and Anthony Widjaja Lin -- Software Model Checking via IC3 / Alessandro Cimatti and Alberto Griggio -- Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits / Călin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin -- Assume-Guarantee Abstraction Refinement for Probabilistic Systems / Anvesh Komuravelli, Corina S. Păsăreanu and Edmund M. Clarke -- Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking / Cyrille Jegourel, Axel Legay and Sean Sedwards -- Timed Relational Abstractions for Sampled Data Control Systems / Aditya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari -- Approximately Bisimilar Symbolic Models for Digital Control Systems / Rupak Majumdar and Majid Zamani -- Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System / Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya and Tiziana Rizzo, et al |
|
Minimum Satisfying Assignments for SMT / Isil Dillig, Thomas Dillig, Kenneth L. McMillan and Alex Aiken -- When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way / Cheng-Shen Han and Jie-Hong Roland Jiang -- A Solver for Reachability Modulo Theories / Akash Lal, Shaz Qadeer and Shuvendu K. Lahiri -- On Decidability of Prebisimulation for Timed Automata / Shibashis Guha, Chinmay Narayan and S. Arun-Kumar -- Exercises in Nonstandard Static Analysis of Hybrid Systems / Ichiro Hasuo and Kohei Suenaga -- A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx / Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan and Andreas Podelski, et al. -- An Axiomatic Memory Model for POWER Multiprocessors / Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian and Jade Alglave, et al. -- nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces / Flavio M. De Paula, Alan J. Hu and Amir Nahir -- Incremental, Inductive CTL Model Checking / Zyad Hassan, Aaron R. Bradley and Fabio Somenzi -- Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement / Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps and Phillip Porras, et al. -- Automatic Quantification of Cache Side-Channels / Boris Köpf, Laurent Mauborgne and Martín Ochoa -- Secure Programming via Visibly Pushdown Safety Games / William R. Harris, Somesh Jha and Thomas Reps |
|
Alternate and Learn: Finding Witnesses without Looking All over / Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan -- A Complete Method for Symmetry Reduction in Safety Verification / Duc-Hiep Chu and Joxan Jaffar -- Synthesizing Number Transformations from Input-Output Examples / Rishabh Singh and Sumit Gulwani -- Acacia+, a Tool for LTL Synthesis / Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin and Jean-François Raskin -- MGSyn: Automatic Synthesis for Industrial Automation / Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll -- OpenNWA: A Nested-Word Automaton Library / Evan Driscoll, Aditya Thakur and Thomas Reps -- Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification / Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik -- SAFARI: SMT-Based Abstraction for Arrays with Interpolants / Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina -- Bma: Visual Tool for Modeling and Analyzing Biological Networks / David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook and Jasmin Fisher, et al. -- APEX: An Analyzer for Open Probabilistic Programs / Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter and James Worrell -- Recent Developments in FDR / Philip Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine and Hristina Palikareva, et al |
|
A Model Checker for Hierarchical Probabilistic Real-Time Systems / Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong -- SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs / Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo -- Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems / Tool Paper / Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout and Fatiha Zaïdi -- HybridSAL Relational Abstracter / Ashish Tiwari -- Euler: A System for Numerical Optimization of Programs / Swarat Chaudhuri and Armando Solar-Lezama -- SPT: Storyboard Programming Tool / Rishabh Singh and Armando Solar-Lezama -- CSolve: Verifying C with Liquid Types / Patrick Rondon, Alexander Bakst, Ming Kawaguchi and Ranjit Jhala -- passert: A Tool for Debugging Parallel Programs / Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik -- TRACER: A Symbolic Execution Tool for Verification / Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa -- Joogie: Infeasible Code Detection for Java / Stephan Arlt and Martin Schäf -- Hector: An Equivalence Checker for a Higher-Order Fragment of ML / David Hopkins, Andrzej S. Murawski and C.-H. Luke Ong -- Resource Aware ML / Jan Hoffmann, Klaus Aehlig and Martin Hofmann |
| Summary |
This book constitutes the refereed proceedings of the 24th International Conference on Computer Aided Verification, CAV 2012, held in Berkeley, CA, USA in July 2012. The 38 regular and 20 tool papers presented were carefully reviewed and selected from 185 submissions. The papers are organized in topical sections on automata and synthesis, inductive inference and termination, abstraction, concurrency and software verification, biology and probabilistic systems, embedded and control systems, SAT/SMT solving and SMT-based verification, timed and hybrid systems, hardware verification, security, verification and synthesis, and tool demonstration |
| Bibliography |
Includes bibliographical references and index |
| Notes |
Print version record |
| Subject |
Computer software -- Verification -- Congresses
|
|
Informatique.
|
|
Computer software -- Verification
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Madhusudan, P.
|
|
Seshia, Sanjit A.
|
| ISBN |
9783642314247 |
|
3642314244 |
|
