![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
22nd CAV 2010: Edinburgh, UK
- Tayssir Touili, Byron Cook, Paul B. Jackson:
Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture Notes in Computer Science 6174, Springer 2010, ISBN 978-3-642-14294-9
Invited Talks
- David A. Basin, Felix Klaedtke, Samuel Müller:
Policy Monitoring in First-Order Temporal Logic. 1-18 - Somesh Jha:
Retrofitting Legacy Code for Security. 19 - Pasquale Malacaria:
Quantitative Information Flow: From Theory to Practice? 20-22 - Maged M. Michael:
Memory Management in Concurrent Algorithms. 23
Invited Tutorials
- Robert K. Brayton, Alan Mishchenko:
ABC: An Academic Industrial-Strength Verification Tool. 24-40 - Thomas W. Reps, Junghee Lim, Aditya V. Thakur, Gogul Balakrishnan, Akash Lal:
There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code. 41-56 - Andrey Rybalchenko:
Constraint Solving for Program Verification: Theory and Practice by Example. 57-71
Software Model Checking
- Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu:
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. 72-88 - Daniel Kroening
, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger
:
Termination Analysis with Compositional Transition Invariants. 89-103 - Kenneth L. McMillan:
Lazy Annotation for Program Testing and Verification. 104-118 - Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg:
The Static Driver Verifier Research Platform. 119-122 - Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala:
Dsolve: Safety Verification via Liquid Types. 123-126 - Sudipta Kundu, Malay K. Ganai, Chao Wang:
Contessa: Concurrency Testing Augmented with Symbolic Analysis. 127-131
Model Checking and Automata
- Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík
, Chih-Duo Hong
, Richard Mayr, Tomás Vojnar
:
Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. 132-147 - Frédéric Herbreteau, B. Srivathsan
, Igor Walukiewicz:
Efficient Emptiness Check for Timed Büchi Automata. 148-161
Tools
- Nicolas Caniart:
Merit: An Interpolating Model-Checker. 162-166 - Alexandre Donzé:
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. 167-170 - Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck:
Jtlv: A Framework for Developing Verification Algorithms. 171-174 - Roland Meyer, Tim Strazny:
Petruchio: From Dynamic Networks to Nets. 175-179
Counter and Hybrid Systems Veri?cation
- Federico Mari
, Igor Melatti, Ivano Salvo, Enrico Tronci
:
Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems. 180-195 - Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, Ernst Moritz Hahn
:
Safety Verification for Probabilistic Hybrid Systems. 196-211 - Khalil Ghorbal, Eric Goubault, Sylvie Putot:
A Logical Product Approach to Zonotope Intersection. 212-226 - Marius Bozga, Radu Iosif, Filip Konecný:
Fast Acceleration of Ultimately Periodic Relations. 227-242 - Luca Pulina
, Armando Tacchella
:
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. 243-257
Memory Consistency
- Jade Alglave, Luc Maranget, Susmit Sarkar
, Peter Sewell
:
Fences in Weak Memory Models. 258-272 - Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin:
Generating Litmus Tests for Contrasting Memory Consistency Models. 273-287
Verification of Hardware and Low Level Code
- Aditya V. Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas W. Reps:
Directed Proof Generation for Machine Code. 288-305 - Christopher L. Conway, Clark W. Barrett
:
Verifying Low-Level Implementations of High-Level Datatypes. 306-320 - Satrajit Chatterjee, Michael Kishinevsky:
Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics. 321-338 - Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin:
Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification. 339-353
Tools
- Stefan Blom, Jaco van de Pol, Michael Weber:
LTSmin: Distributed and Symbolic Reachability. 354-359 - Benedikt Bollig, Joost-Pieter Katoen
, Carsten Kern, Martin Leucker
, Daniel Neider
, David R. Piegdon:
libalf: The Automata Learning Framework. 360-364
Synthesis
- Rüdiger Ehlers
:
Symbolic Bounded Synthesis. 365-379 - Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh:
Measuring and Synthesizing Systems in Probabilistic Environments. 380-395 - Susanne Graf, Doron A. Peled, Sophie Quinton:
Achieving Distributed Control through Model Checking. 396-409 - Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann:
Robustness in the Presence of Liveness. 410-424 - Roderick Bloem, Alessandro Cimatti
, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri
, Viktor Schuppan, Richard Seeber:
RATSY - A New Requirements Analysis Tool with Synthesis. 425-429 - Viktor Kuncak, Mikaël Mayer, Ruzica Piskac
, Philippe Suter:
Comfusy: A Tool for Complete Functional Synthesis. 430-433
Concurrent Program Verification I
- Vineet Kahlon, Chao Wang:
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs. 434-449 - Viktor Vafeiadis
:
Automatically Proving Linearizability. 450-464 - Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, Rajeev Alur:
Model Checking of Linearizability of Concurrent List Implementations. 465-479 - Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies:
Local Verification of Global Invariants in Concurrent Programs. 480-494 - Aws Albarghouthi, Arie Gurfinkel
, Ou Wei, Marsha Chechik:
Abstract Analysis of Symbolic Executions. 495-510
Compositional Reasoning
- Yu-Fang Chen
, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay
, Bow-Yaw Wang:
Automated Assume-Guarantee Reasoning through Implicit Learning. 511-526 - Rishabh Singh, Dimitra Giannakopoulou, Corina S. Pasareanu:
Learning Component Interfaces with May and Must Abstractions. 527-542 - Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar:
A Dash of Fairness for Compositional Reasoning. 543-557 - Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar:
SPLIT: A Compositional LTL Verifier. 558-561
Tools
- Marco Bozzano, Alessandro Cimatti
, Joost-Pieter Katoen
, Viet Yen Nguyen, Thomas Noll
, Marco Roveri
, Ralf Wimmer
:
A Model Checker for AADL. 562-565 - Manuel Mazo Jr.
, Anna Davitian, Paulo Tabuada
:
PESSOA: A Tool for Embedded Controller Synthesis. 566-569
Decision Procedures
- Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu:
On Array Theory of Bounded Elements. 570-584 - David Monniaux:
Quantifier Elimination by Lazy Model Enumeration. 585-599
Concurrent Program Verification II
- Pierre Ganty, Rupak Majumdar, Benjamin Monmege
:
Bounded Underapproximations. 600-614 - Anil Seth:
Global Reachability in Bounded Phase Multi-stack Pushdown Systems. 615-628 - Salvatore La Torre, P. Madhusudan, Gennaro Parlato
:
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. 629-644 - Alexander Kaiser, Daniel Kroening
, Thomas Wahl:
Dynamic Cutoff Detection in Parameterized Concurrent Programs. 645-659
Tools
- Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang:
PARAM: A Model Checker for Parametric Markov Models. 660-664 - Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna:
Gist: A Solver for Probabilistic Games. 665-669 - Alessandro Ferrante, Maurizio Memoli, Margherita Napoli
, Mimmo Parente
, Francesco Sorrentino:
A NuSMV Extension for Graded-CTL Model Checking. 670-673
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.