Shuvendu K. Lahiri

Thomas W. Reps

Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 2020

Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost.

[BibT_eX]

[DOI]

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

2019

Abstract semantic diffing of evolving concurrent programs.

[BibT_eX]

[DOI]

Ahmed Bouajjani

Constantin Enea

Formal Methods Syst. Des., 2019

Enabling Open-World Specification Mining via Unsupervised Learning.

[BibT_eX]

[DOI]

CoRR, 2019

Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2019

2018

Artifact for Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces.

[BibT_eX]

[DOI]

Dataset, August, 2018

Artifact for Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces.

[BibT_eX]

[DOI]

Dataset, June, 2018

Artifact for Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces.

[BibT_eX]

[DOI]

Dataset, June, 2018

Verified three-way program merge.

[BibT_eX]

[DOI]

Marcelo Sousa

Isil Dillig

Proc. ACM Program. Lang., 2018

Verifying equivalence of database-driven applications.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Verifying Relative Safety, Accuracy, and Termination for Program Approximations.

[BibT_eX]

[DOI]

Shaobo He

Zvonimir Rakamaric

J. Autom. Reason., 2018

Wireless protocol validation under uncertainty.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2018

Program Equivalence (Dagstuhl Seminar 18151).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2018

Formal Specification and Verification of Smart Contracts for Azure Blockchain.

[BibT_eX]

[DOI]

CoRR, 2018

VeriFi: Model-Driven Runtime Verification Framework for Wireless Protocol Implementations.

[BibT_eX]

[DOI]

CoRR, 2018

Verifying Semantic Conflict-Freedom in Three-Way Program Merges.

[BibT_eX]

[DOI]

Marcelo Sousa

Isil Dillig

CoRR, 2018

Code vectors: understanding programs through embedded abstracted symbolic traces.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018

Datalog-based scalable semantic diffing of concurrent programs.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

2017

Refining interprocedural change-impact analysis using equivalence relations.

[BibT_eX]

[DOI]

Alex Gyori

Nimrod Partush

Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10, 2017

Optimizing test placement for module-level regression testing.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Modular Verification of Procedure Equivalence in the Presence of Memory Allocation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

2016

Interprocedural Semantic Change-Impact Analysis using Equivalence Relations.

[BibT_eX]

[DOI]

Alex Gyori

Nimrod Partush

CoRR, 2016

2015

Helping Developers Help Themselves: Automatic Decomposition of Code Review Changesets.

[BibT_eX]

[DOI]

Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Automatic Rootcausing for Program Equivalence Failures in Binaries.

[BibT_eX]

[DOI]

Rohit Sinha

Chris Hawblitzel

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Angelic Verification: Precise Verification Modulo Unknowns.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Verification modulo versions: towards usable verification.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

2013

Towards Practical Reactive Security Audit Using Extended Static Checkers.

[BibT_eX]

[DOI]

Julien Vanegue

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Differential assertion checking.

[BibT_eX]

[DOI]

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Will you still compile me tomorrow? static cross-version compiler validation.

[BibT_eX]

[DOI]

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Almost-correct specifications: a modular semantic framework for assigning confidence to warnings.

[BibT_eX]

[DOI]

Sam Blackshear

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Towards Modularly Comparing Programs Using Automated Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Underspecified harnesses and interleaved bugs.

[BibT_eX]

[DOI]

Saurabh Joshi

Akash Lal

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

A Solver for Reachability Modulo Theories.

[BibT_eX]

[DOI]

Akash Lal

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

SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs.

[BibT_eX]

[DOI]

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

2011

ExplainHoudini: Making Houdini Inference Transparent.

[BibT_eX]

[DOI]

Julien Vanegue

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation.

[BibT_eX]

[DOI]

Patrice Godefroid

Cindy Rubio-González

Proceedings of the Static Analysis - 18th International Symposium, 2011

Linear maps.

[BibT_eX]

[DOI]

David Walker

Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, 2011

Call Invariants.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods, 2011

From Program to Logic: An Introduction.

[BibT_eX]

[DOI]

Patrice Godefroid

Proceedings of the Tools for Practical Software Verification, 2011

SMT-Based Modular Analysis of Sequential Systems Code.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Towards Scalable Modular Checking of User-Defined Properties.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2010

Abstract Threads.

[BibT_eX]

[DOI]

Alexander Malkis

Proceedings of the Verification, 2010

Differential static analysis: opportunities, applications, and challenges.

[BibT_eX]

[DOI]

Kapil Vaswani

C. A. R. Hoare

Proceedings of the Workshop on Future of Software Engineering Research, 2010

2009

A low-level memory model and an accompanying reachability predicate.

[BibT_eX]

[DOI]

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

Unifying type checking and property checking for low-level code.

[BibT_eX]

[DOI]

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers.

[BibT_eX]

[DOI]

Zvonimir Rakamaric

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Intra-module Inference.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Complexity and Algorithms for Monomial and Clausal Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Back to the future: revisiting precise program verification using SMT solvers.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Finding errors in .net with feedback-directed random testing.

[BibT_eX]

[DOI]

Carlos Pacheco

Thomas Ball

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

Embedded software verification: challenges and solutions.

[BibT_eX]

[DOI]

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

2007

Predicate abstraction with indexed predicates.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2007

Predicate Abstraction via Symbolic Decision Procedures.

[BibT_eX]

[DOI]

Thomas Ball

Byron Cook

Log. Methods Comput. Sci., 2007

Interpolant based Decision Procedure for Quantifier-Free Presburger Arithmetic.

[BibT_eX]

[DOI]

Krishna K. Mehra

J. Satisf. Boolean Model. Comput., 2007

A Reachability Predicate for Analyzing Low-Level Software.

[BibT_eX]

[DOI]

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

Feedback-Directed Random Test Generation.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

2006

Verifying properties of well-founded linked lists.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

SMT Techniques for Fast Predicate Abstraction.

[BibT_eX]

[DOI]

Robert Nieuwenhuis

Albert Oliveras

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Solving Sparse Linear Constraints.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Zap: Automated Theorem Proving for Software Analysis.

[BibT_eX]

[DOI]

Thomas Ball

Proceedings of the Logic for Programming, 2005

An Efficient Decision Procedure for UTVPI Constraints.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

2004

Constructing Quantified Invariants via Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2004

Revisiting Positive Equality.

[BibT_eX]

[DOI]

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

The UCLID Decision Procedure.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Indexed Predicate Discovery for Unbounded System Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

A hybrid SAT-based decision procedure for separation logic with uninterpreted functions.

[BibT_eX]

[DOI]

Proceedings of the 40th Design Automation Conference, 2003

Convergence Testing in Term-Level Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

A Symbolic Approach to Predicate Abstraction.

[BibT_eX]

[DOI]

Byron Cook

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Deductive Verification of Advanced Out-of-Order Microprocessors.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

Modeling and Verification of Out-of-Order Microprocessors in UCLID.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Experience with term level modeling and verification of the M*CORE <sup>TM</sup> microprocessor core.

[BibT_eX]

[DOI]