Natasha Sharygina

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

LRA Interpolants from No Man's Land.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2017

Designing parallel PDR.

[BibT_eX]

[DOI]

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Duality-based interpolation for quantifier-free equalities and uninterpreted functions.

[BibT_eX]

[DOI]

Sepideh Asadi

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

OpenSMT2: An SMT Solver for Multi-core and Cloud Computing.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

PVAIR: Partial Variable Assignment InterpolatoR.

[BibT_eX]

[DOI]

Pavel Jancík

Jan Kofron

Proceedings of the Fundamental Approaches to Software Engineering, 2016

Property Directed Equivalence via Abstract Simulation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Clause Sharing and Partitioning for Cloud-Based SMT Solving.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

Decision Procedures for Flat Array Properties.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

A Proof-Sensitive Approach for Small Propositional Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Search-Space Partitioning for Parallelizing SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Flexible Interpolation for Efficient Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Mathematical and Engineering Methods in Computer Science, 2015

Automated Discovery of Simulation Between Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A New Acceleration-Based Combination Framework for Array Properties.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Symbolic Detection of Assertion Dependencies for Bounded Model Checking.

[BibT_eX]

[DOI]

Andrea Callia D'Iddio

Proceedings of the Fundamental Approaches to Software Engineering, 2015

Incremental Upgrade Checking.

[BibT_eX]

[DOI]

Proceedings of the Validation of Evolving Software, 2015

Function Summarization-Based Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Validation of Evolving Software, 2015

Optimizing Function Summaries Through Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Validation of Evolving Software, 2015

Regression Checking of Changes in C Software.

[BibT_eX]

[DOI]

Fabrizio Pastore

Leonardo Mariani

Proceedings of the Validation of Evolving Software, 2015

Complementarities Among the Technologies Presented in the Book.

[BibT_eX]

[DOI]

Proceedings of the Validation of Evolving Software, 2015

Challenges of Existing Technology.

[BibT_eX]

[DOI]

Proceedings of the Validation of Evolving Software, 2015

Introduction.

[BibT_eX]

[DOI]

Proceedings of the Validation of Evolving Software, 2015

2014

Resolution proof transformation for compression and interpolation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

An extension of lazy abstraction with interpolation for programs with arrays.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

Monotonic Abstraction Techniques: from Parametric to Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Logics and Model-checking for Self-* Systems, 2014

Verige: verification with invariant generation engine.

[BibT_eX]

[DOI]

Nicolas Latorre

Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods: Foundations and Applications - 17th Brazilian Symposium, 2014

Incremental Verification of Compiler Optimizations.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Verification-aided regression testing.

[BibT_eX]

[DOI]

Fabrizio Pastore

Leonardo Mariani

Proceedings of the International Symposium on Software Testing and Analysis, 2014

On interpolants and variable assignments.

[BibT_eX]

[DOI]

Pavel Jancík

Jan Kofron

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Booster: An Acceleration-Based Verification Framework for Array Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Loop summarization using state and transition invariants.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Abstraction and Acceleration in SMT-based Model-Checking for Array Programs

[BibT_eX]

[DOI]

CoRR, 2013

eVolCheck: Incremental Upgrade Checker for C.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Using cross-entropy for satisfiability.

[BibT_eX]

[DOI]

Hana Chockler

Alexander Ivrii

Arie Matsliah

Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013

A Parametric Interpolation Framework for First-Order Theories.

[BibT_eX]

[DOI]

Laura Kovács

Proceedings of the Advances in Artificial Intelligence and Its Applications, 2013

PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Acceleration-based safety decision procedure for programs with arrays.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

Definability of Accelerated Relations in a Theory of Arrays and Its Applications.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

Interpolation-based model checking for efficient incremental analysis of software.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, 2013

PINCETTE - Validating Changes and Upgrades in Networked Software.

[BibT_eX]

[DOI]

Proceedings of the 17th European Conference on Software Maintenance and Reengineering, 2013

Interpolation Properties and SAT-Based Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

An abstraction refinement approach combining precise and approximated techniques.

[BibT_eX]

[DOI]

Stefano Tonetta

Int. J. Softw. Tools Technol. Transf., 2012

Propositional Interpolation Systems for Model Checking

[BibT_eX]

[DOI]

CoRR, 2012

Lazy Abstraction with Interpolants for Arrays.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Incremental upgrade checking by means of interpolation-based function summaries.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2012

Leveraging Interpolant Strength in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

SAFARI: SMT-Based Abstraction for Arrays with Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Reachability Modulo Theory Library.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2012

2011

A model checking-based approach for security policy verification of mobile systems.

[BibT_eX]

[DOI]

Chiara Braghin

Katerina Barone-Adesi

Formal Aspects Comput., 2011

Loop Summarization and Termination Analysis.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Interpolation-Based Function Summaries in Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

Function Summaries in Software Upgrade Checking.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

2010

The OpenSMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

A flexible schema for generating explanations in lazy theory propagation.

[BibT_eX]

[DOI]

Edgar Pek

Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Flexible interpolation with local proof transformations.

[BibT_eX]

[DOI]

Proceedings of the 2010 International Conference on Computer-Aided Design, 2010

An Efficient and Flexible Approach to Resolution Proof Reduction.

[BibT_eX]

[DOI]

Simone Rollini

Proceedings of the Hardware and Software: Verification and Testing, 2010

Termination Analysis with Compositional Transition Invariants.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Loopfrog - loop summarization for static analysis.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Invariant Generation, 2010

2009

An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk.

[BibT_eX]

[DOI]

Stefano Tonetta

Proceedings of the SAVCBS'09, 2009

The synergy of precise and fast abstractions for program verification.

[BibT_eX]

[DOI]

Stefano Tonetta

Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

Loopfrog: A Static Analyzer for ANSI-C Programs.

[BibT_eX]

[DOI]

Proceedings of the ASE 2009, 2009

A scalable decision procedure for fixed-width bit-vectors.

[BibT_eX]

[DOI]

Proceedings of the 2009 International Conference on Computer-Aided Design, 2009

2008

Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Verification of evolving software via component substitutability analysis.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2008

Scoot: A Tool for the Analysis of SystemC Models.

[BibT_eX]

[DOI]

Nicolas Blanc

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Loop Summarization Using Abstract Transformers.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

Verification of Boolean programs with unbounded thread creation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

VCEGAR: Verilog CounterExample Guided Abstraction Refinement.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Model Checking with Abstraction for Web Services.

[BibT_eX]

[DOI]

Daniel Kröning

Proceedings of the Test and Analysis of Web Services, 2007

Specification and verification of component-based systems 2007.

[BibT_eX]

[DOI]

Jonathan Aldrich

Michael Barnett

Dimitra Giannakopoulou

Gary T. Leavens

Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007

Automated Verification of Security Policies in Mobile Code.

[BibT_eX]

[DOI]

Chiara Braghin

Katerina Barone-Adesi

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs.

[BibT_eX]

[DOI]

Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

2006

Approximating Predicate Images for Bit-Vector Logic.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Over-Approximating Boolean Programs with Unbounded Thread Creation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

2005

Concurrent software verification with states, events, and deadlocks.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2005

SATABS: SAT-Based Predicate Abstraction for ANSI-C.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Symbolic Model Checking for Asynchronous Boolean Programs.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2005

Formal verification of SystemC by automatic hardware/software partitioning.

[BibT_eX]

[DOI]

Proceedings of the 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 2005

State/Event Software Verification for Branching-Time Specifications.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 5th International Conference, 2005

Program Compatibility Approaches.

[BibT_eX]

[DOI]

Edmund M. Clarke

Nishant Sinha

Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Dynamic Component Substitutability Analysis.

[BibT_eX]

[DOI]

Proceedings of the FM 2005: Formal Methods, 2005

Word level predicate abstraction and refinement for verifying RTL verilog.

[BibT_eX]

[DOI]

Proceedings of the 42nd Design Automation Conference, 2005

Cogent: Accurate Theorem Proving for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The ComFoRT Reasoning Framework.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Lessons Learned from Model Checking a NASA Robot Controller.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2004

Guest Editorial.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2004

Predicate Abstraction of ANSI-C Programs Using SAT.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2004

Automated, compositional and iterative deadlock detection.

[BibT_eX]

[DOI]

Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Accurate Theorem Proving for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, 2004

State/Event-Based Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

2003

Model Checking Software via Abstraction of Loop Transitions.

[BibT_eX]

[DOI]

James C. Browne

Proceedings of the Fundamental Approaches to Software Engineering, 2003

2001

A Combined Testing and Verification Approach for Software Reliability.

[BibT_eX]

[DOI]

Doron A. Peled

Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001

A Formal Object-Oriented Analysis for Software Reliability: Design for Verification.

[BibT_eX]

[DOI]