Corral Program Verifier

Established: May 9, 2013

Publications

View by:

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

Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal

FMCAD | July 2020

Best paper award

Publication Video Project

Distributed Bounded Model Checking

Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal

FMCAD | July 2020

Publication Video
Precise null-pointer analysis using Global Value Numbering

Ankush Das, Akash Lal

Automated Technology for Verification and Analysis (ATVA) | July 2017

Publication Project
Inferring Annotations For Device Drivers From Verification Histories

Zvonimir Pavlinovic, Akash Lal, Rahul Sharma

Automated Software Engineering (ASE) | September 2016

ACM SIGSOFT Distinguished Paper Award

Publication

Inferring Annotations For Device Drivers From Verification Histories

Zvonimir Pavlinovic, Akash Lal, Rahul Sharma

MSR-TR-2016-15 | April 2016

Publication
Angelic Verification: Precise Verification Modulo Unknowns

Shuvendu Lahiri, Akash Lal, Yi Li, Ankush Das

Computer Aided Verification (CAV) | July 2015

Publication Publication Project

DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs

Akash Lal, Shaz Qadeer

Programming Language Design and Implementation (PLDI) | June 2015

Publication

SMACK+Corral: A Modular Verifier (Competition Contribution)

Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric

Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | March 2015

Publication
Powering the Static Driver Verifier using Corral

Akash Lal, Shaz Qadeer

Foundations of Software Engineering (FSE) | November 2014

ACM SIGSOFT Distinguished Paper

Publication Download

A Program Transformation for Faster Goal-Directed Search

Akash Lal, Shaz Qadeer

Formal Methods in Computer-Aided Design (FMCAD) | October 2014

Best Paper Award

Publication
Reachability Modulo Theories

Akash Lal, Shaz Qadeer

7th International workshop on Reachability Problems (Invited Paper) | September 2013

Publication
Finding Non-Terminating Executions in Distributed Asynchronous Programs

Michael Emmi, Akash Lal

Static Analysis Symposium (SAS) | September 2012

Publication

Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

Computer-Aided Verification (CAV) | July 2012

Computer-Aided Verification (CAV)

Publication

Asynchronous programs with prioritized task buffers

Michael Emmi, Akash Lal, Shaz Qadeer

MSR-TR-2012-1 | January 2012

Publication

Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

MSR-TR-2012-9 | January 2012

Publication

Underspecified Harnesses and Interleaved Bugs

Saurabh Joshi, Shuvendu Lahiri, Akash Lal

Principles of Programming Languages (POPL) 2012 | January 2012

Publication Project Project
Delay-bounded scheduling

Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric

Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages | January 2011

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

Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric

Computer Aided Verification (CAV '09) | February 2009

Publication Project Project

Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

Akash Lal, Thomas Reps

Formal Methods in System Design (FMSD) | January 2009

Publication

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

Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal

FMCAD | July 2020

Best paper award

Publication Video Project

Distributed Bounded Model Checking

Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal

FMCAD | July 2020

Publication Video

Precise null-pointer analysis using Global Value Numbering

Ankush Das, Akash Lal

Automated Technology for Verification and Analysis (ATVA) | July 2017

Publication Project

Inferring Annotations For Device Drivers From Verification Histories

Zvonimir Pavlinovic, Akash Lal, Rahul Sharma

Automated Software Engineering (ASE) | September 2016

ACM SIGSOFT Distinguished Paper Award

Publication

Inferring Annotations For Device Drivers From Verification Histories

Zvonimir Pavlinovic, Akash Lal, Rahul Sharma

MSR-TR-2016-15 | April 2016

Publication

Angelic Verification: Precise Verification Modulo Unknowns

Shuvendu Lahiri, Akash Lal, Yi Li, Ankush Das

Computer Aided Verification (CAV) | July 2015

Publication Publication Project

DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs

Akash Lal, Shaz Qadeer

Programming Language Design and Implementation (PLDI) | June 2015

Publication

SMACK+Corral: A Modular Verifier (Competition Contribution)

Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric

Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | March 2015

Publication

Powering the Static Driver Verifier using Corral

Akash Lal, Shaz Qadeer

Foundations of Software Engineering (FSE) | November 2014

ACM SIGSOFT Distinguished Paper

Publication Download

A Program Transformation for Faster Goal-Directed Search

Akash Lal, Shaz Qadeer

Formal Methods in Computer-Aided Design (FMCAD) | October 2014

Best Paper Award

Publication

Reachability Modulo Theories

Akash Lal, Shaz Qadeer

7th International workshop on Reachability Problems (Invited Paper) | September 2013

Publication

Finding Non-Terminating Executions in Distributed Asynchronous Programs

Michael Emmi, Akash Lal

Static Analysis Symposium (SAS) | September 2012

Publication

Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

Computer-Aided Verification (CAV) | July 2012

Computer-Aided Verification (CAV)

Publication

Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

MSR-TR-2012-9 | January 2012

Publication

Underspecified Harnesses and Interleaved Bugs

Saurabh Joshi, Shuvendu Lahiri, Akash Lal

Principles of Programming Languages (POPL) 2012 | January 2012

Publication Project Project

Asynchronous programs with prioritized task buffers

Michael Emmi, Akash Lal, Shaz Qadeer

MSR-TR-2012-1 | January 2012

Publication

Delay-bounded scheduling

Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric

Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages | January 2011

Publication

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

Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric

Computer Aided Verification (CAV '09) | February 2009

Publication Project Project

Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

Akash Lal, Thomas Reps

Formal Methods in System Design (FMSD) | January 2009

Publication
Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

Computer-Aided Verification (CAV) | July 2012

Computer-Aided Verification (CAV)

Publication

Asynchronous programs with prioritized task buffers

Michael Emmi, Akash Lal, Shaz Qadeer

MSR-TR-2012-1 | January 2012

Publication

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

Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal

FMCAD | July 2020

Best paper award

Publication Video Project

Distributed Bounded Model Checking

Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal

FMCAD | July 2020

Publication Video

Precise null-pointer analysis using Global Value Numbering

Ankush Das, Akash Lal

Automated Technology for Verification and Analysis (ATVA) | July 2017

Publication Project

Inferring Annotations For Device Drivers From Verification Histories

Zvonimir Pavlinovic, Akash Lal, Rahul Sharma

Automated Software Engineering (ASE) | September 2016

ACM SIGSOFT Distinguished Paper Award

Publication

Angelic Verification: Precise Verification Modulo Unknowns

Shuvendu Lahiri, Akash Lal, Yi Li, Ankush Das

Computer Aided Verification (CAV) | July 2015

Publication Publication Project

DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs

Akash Lal, Shaz Qadeer

Programming Language Design and Implementation (PLDI) | June 2015

Publication

SMACK+Corral: A Modular Verifier (Competition Contribution)

Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric

Tools and Algorithms for the Construction and Analysis of Systems (TACAS) | March 2015

Publication

Powering the Static Driver Verifier using Corral

Akash Lal, Shaz Qadeer

Foundations of Software Engineering (FSE) | November 2014

ACM SIGSOFT Distinguished Paper

Publication Download

A Program Transformation for Faster Goal-Directed Search

Akash Lal, Shaz Qadeer

Formal Methods in Computer-Aided Design (FMCAD) | October 2014

Best Paper Award

Publication

Reachability Modulo Theories

Akash Lal, Shaz Qadeer

7th International workshop on Reachability Problems (Invited Paper) | September 2013

Publication

Finding Non-Terminating Executions in Distributed Asynchronous Programs

Michael Emmi, Akash Lal

Static Analysis Symposium (SAS) | September 2012

Publication

Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

Computer-Aided Verification (CAV) | July 2012

Computer-Aided Verification (CAV)

Publication

Underspecified Harnesses and Interleaved Bugs

Saurabh Joshi, Shuvendu Lahiri, Akash Lal

Principles of Programming Languages (POPL) 2012 | January 2012

Publication Project Project

Delay-bounded scheduling

Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric

Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages | January 2011

Publication

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

Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric

Computer Aided Verification (CAV '09) | February 2009

Publication Project Project
Inferring Annotations For Device Drivers From Verification Histories

Zvonimir Pavlinovic, Akash Lal, Rahul Sharma

MSR-TR-2016-15 | April 2016

Publication

Corral: A Solver for Reachability Modulo Theories

Akash Lal, Shaz Qadeer, Shuvendu Lahiri

MSR-TR-2012-9 | January 2012

Publication

Asynchronous programs with prioritized task buffers

Michael Emmi, Akash Lal, Shaz Qadeer

MSR-TR-2012-1 | January 2012

Publication
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

Akash Lal, Thomas Reps

Formal Methods in System Design (FMSD) | January 2009

Publication

People

Shuvendu Lahiri

Senior Principal Researcher

Learn more

Akash Lal

Senior Principal Researcher

Learn more

Corral Program Verifier

Publications

Publications by Year

2020

2017

2016

2015

2014

2013

2012

2011

2009

Publications by Research Area

Programming languages and software engineering

Systems and networking

Publications by Type

Inproceedings (Conference)

Tech Report

Article (Journal)

People

Shuvendu Lahiri

Akash Lal