Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna |
Gist: A Solver for Probabilistic Games. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz |
Efficient Emptiness Check for Timed Büchi Automata. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Viktor Vafeiadis |
Automatically Proving Linearizability. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck |
Jtlv: A Framework for Developing Verification Algorithms. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Aditya V. Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas W. Reps |
Directed Proof Generation for Machine Code. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Ariel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa'ar |
A Dash of Fairness for Compositional Reasoning. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Rishabh Singh, Dimitra Giannakopoulou, Corina S. Pasareanu |
Learning Component Interfaces with May and Must Abstractions. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Manuel Mazo Jr., Anna Davitian, Paulo Tabuada |
PESSOA: A Tool for Embedded Controller Synthesis. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Blom, Jaco van de Pol, Michael Weber 0002 |
LTSmin: Distributed and Symbolic Reachability. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Yu-Fang Chen 0001, 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. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Kaiser 0001, Daniel Kroening, Thomas Wahl |
Dynamic Cutoff Detection in Parameterized Concurrent Programs. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
Lazy Annotation for Program Testing and Verification. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger |
Termination Analysis with Compositional Transition Invariants. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Somesh Jha |
Retrofitting Legacy Code for Security. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | David Monniaux |
Quantifier Elimination by Lazy Model Enumeration. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Tayssir Touili, Byron Cook, Paul B. Jackson (eds.) |
Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis |
D-Finder: A Tool for Compositional Deadlock Detection and Verification. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Azadeh Farzan, P. Madhusudan, Francesco Sorrentino 0002 |
Meta-analysis for Atomicity Violations under Nested Locking. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Swen Jacobs |
Incremental Instance Generation in Local Reasoning. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Rachid Guerraoui, Michal Kapalka |
Transactional Memory: Glimmer of a Theory. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Nathan Kitchen, Andreas Kuehlmann |
A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh |
Software Transactional Memory on Relaxed Memory Models. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Oded Fuhrmann, Shlomo Hoory |
On Extending Bounded Proofs to Inductive Proofs. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
resolution proofs, extending proofs, proof simplification, Formal verification |
1 | Joseph Sifakis |
Component-Based Construction of Real-Time Systems in BIP. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe |
Towards Performance Prediction of Compositional Models in Industrial GALS Designs. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Nikolaj S. Bjørner, Joe Hendrix |
Linear Functional Fixed-points. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Pavol Cerný, Rajeev Alur |
Automated Analysis of Java Methods for Confidentiality. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | David Monniaux |
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Bertrand Jeannet, Antoine Miné |
Apron: A Library of Numerical Abstract Domains for Static Analysis. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv |
Generalizing DPLL to Richer Logics. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Thao Dang 0001, David Salinas |
Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Marco Roveri, Stefano Tonetta |
Requirements Validation for Hybrid Systems. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, Franck Védrine |
HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jie-Hong R. Jiang |
Quantifier Elimination via Functional Composition. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Yeting Ge, Leonardo Mendonça de Moura |
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | David Hopkins 0002, C.-H. Luke Ong |
Homer: A Higher-Order Observational Equivalence Model checkER. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric |
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir A. Frolov, Erik Reeber, Armaghan Naik |
Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Ananda Basu, Saddek Bensalem, Doron A. Peled, Joseph Sifakis |
Priority Scheduling of Distributed Systems Based on Model Checking. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Alessio Lomuscio, Hongyang Qu 0001, Franco Raimondi |
MCMAS: A Model Checker for the Verification of Multi-Agent Systems. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Vineet Kahlon, Chao Wang 0001, Aarti Gupta |
Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura |
A Concurrent Portfolio Approach to SMT Solving. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Ahmed Bouajjani, Oded Maler (eds.) |
Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Amir M. Ben-Amram |
Size-Change Termination, Monotonicity Constraints and Ranking Functions. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Pallavi Joshi, Mayur Naik, Chang-Seo Park, Koushik Sen |
CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Minxue Pan, Lei Bu, Xuandong Li |
TASS: Timing Analyzer of Scenario-Based Specifications. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh |
Models and Proofs of Protocol Security: A Progress Report. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecný, Tomás Vojnar |
Automatic Verification of Integer Array Programs. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe |
Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Ofer Strichman |
Regression Verification: Proving the Equivalence of Similar Programs. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Luca Benini |
Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Colas Le Guernic, Antoine Girard |
Reachability Analysis of Hybrid Systems Using Support Functions. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sylvain Hallé, Roger Villemaire |
Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Michael Ryabtsev, Ofer Strichman |
Translation Validation: From Simulink to C. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang 0001 |
INFAMY: An Infinite-State Markov Model Checker. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler |
Explaining Counterexamples Using Causality. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh 0002, Sriram Sankaranarayanan 0001, K. C. Shashidhar |
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Peter Lammich, Markus Müller-Olm, Alexander Wenner |
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jaeha Kim |
Mixed-Signal System Verification: A High-Speed Link Example. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
analog and mixed-signal verification, analog design intent, linear system models |
1 | Thomas Gawlitza, Helmut Seidl |
Games through Nested Fixpoints. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sumit Gulwani |
SPEED: Symbolic Complexity Bound Analysis. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Khalil Ghorbal, Eric Goubault, Sylvie Putot |
The Zonotope Abstract Domain Taylor1+. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
Symbolic Counter Abstraction for Concurrent Software. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh |
Cardinality Abstraction for Declarative Networking Applications. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jean Krivine, Vincent Danos, Arndt Benecke |
Modelling Epigenetic Information Maintenance: A Kappa Tutorial. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia |
Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann |
Better Quality in Synthesis through Quantitative Objectives. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Ashutosh Gupta 0001, Andrey Rybalchenko |
InvGen: An Efficient Invariant Generator. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Rupak Majumdar, Ru-Gang Xu |
Reducing Test Inputs Using Information Partitions. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Saurabh Srivastava 0001, Sumit Gulwani, Jeffrey S. Foster |
VS3: SMT Solvers for Program Verification. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Warren A. Hunt Jr., Sol Swords |
Centaur Technology Media Unit Verification. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jun Sun 0001, Yang Liu 0003, Jin Song Dong, Jun Pang 0001 |
PAT: Towards Flexible Verification under Fairness. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Isil Dillig, Thomas Dillig, Alex Aiken |
Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies |
Intra-module Inference. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Thomas A. Henzinger, Maria Mateescu, Verena Wolf |
Sliding Window Abstraction for Infinite Markov Chains. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Emmanuel Filiot, Naiyong Jin, Jean-François Raskin |
An Antichain Algorithm for LTL Realizability. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Podelski, Andrey Rybalchenko, Thomas Wies |
Heap Assumptions on Demand. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Himanshu Jain, Edmund M. Clarke, Orna Grumberg |
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Stephen Magill, Ming-Hsien Tsai 0001, Peter Lee 0001, Yih-Kuen Tsay |
THOR: A Tool for Reasoning about Shape and Arithmetic. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani |
The MathSAT 4SMT Solver. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel |
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Kinder, Helmut Veith |
Jakstab: A Static Analysis Platform for Binaries. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Sujatha Kashyap, Vijay K. Garg |
Producing Short Counterexamples Using "Crucial Events". |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Sudipta Kundu, Sorin Lerner, Rajesh Gupta 0001 |
Validating High-Level Synthesis. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Andy King, Harald Søndergaard |
Inferring Congruence Equations Using SAT. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Akash Lal, Thomas W. Reps |
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Reinhard Wilhelm, Björn Wachter |
Abstract Interpretation with Applications to Timing Validation. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby |
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Harry Foster |
Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial). |
CAV |
2008 |
DBLP DOI BibTeX RDF |
Simulation, Formal Verification, Debugging, Assertion, Functional Verification, Property Specification, Assertion-Based Verification |
1 | Sumit Gulwani, Ashish Tiwari 0001 |
Constraint-Based Approach for Analysis of Hybrid Systems. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Michael Backes 0001, Stefan Lorenz, Matteo Maffei, Kim Pecina |
The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Rob J. van Glabbeek, Bas Ploeger |
Correcting a Space-Efficient Simulation Algorithm. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Axel Legay |
T(O)RMC: A Tool for (omega)-Regular Model Checking. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | André Platzer, Edmund M. Clarke |
Computing Differential Invariants of Hybrid Systems as Fixedpoints. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
verification of hybrid systems, verification logic, fixedpoint engine, differential invariants |
1 | John Harrison 0001 |
Theorem Proving for Verification (Invited Tutorial). |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, Andreas Podelski |
Faster Than Uppaal? |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Salil Joshi 0002, Barbara König 0001 |
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Cindy Eisner, Amir Nahir, Karen Yorav |
Functional Verification of Power Gated Designs by Compositional Reasoning. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Cas J. F. Cremers |
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|