Efficient Filtering in Publish-Subscribe Systems Using Binary Decision. - Alexis Campailla; Sagar Chaki; Edmund M. Clarke; Somesh Jha; Helmut Veith (ICSE, 2001)

Parameterized Verification of Multithreaded Software Libraries. - Thomas Ball 001; Sagar Chaki; Sriram K. Rajamani (TACAS, 2001)

Types as models: model checking message-passing programs. - Sagar Chaki; Sriram K. Rajamani; Jakob Rehof (POPL, 2002)

Predicate Abstraction with Minimum Predicates. - Sagar Chaki; Edmund M. Clarke; Alex Groce; Ofer Strichman (CHARME, 2003)

Integrating Publish/Subscribe into a Mobile Teamwork Support Platform. - Sagar Chaki; Pascal Fenkam; Harald C. Gall; Somesh Jha; Engin Kirda; Helmut Veith (SEKE, 2003)

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. - Sagar Chaki; Joël Ouaknine; Karen Yorav; Edmund M. Clarke (SoftMC@CAV, 2003)

State/Event-Based Software Model Checking. - Sagar Chaki; Edmund M. Clarke; Joël Ouaknine; Natasha Sharygina; Nishant Sinha 001 (IFM, 2004)

Automated, compositional and iterative deadlock detection. - Sagar Chaki; Edmund M. Clarke; Joël Ouaknine; Natasha Sharygina (MEMOCODE, 2004)

Explaining abstract counterexamples. - Sagar Chaki; Alex Groce; Ofer Strichman (SIGSOFT FSE, 2004)

Efficient Verification of Sequential and Concurrent C Programs. - Sagar Chaki; Edmund M. Clarke; Alex Groce; Joël Ouaknine; Ofer Strichman; Karen Yorav (Formal Methods Syst. Des., 2004)

Modular Verification of Software Components in C. - Sagar Chaki; Edmund M. Clarke; Alex Groce; Somesh Jha; Helmut Veith (IEEE Trans. Software Eng., 2004)

Automated Assume-Guarantee Reasoning for Simulation Conformance. - Sagar Chaki; Edmund M. Clarke; Nishant Sinha 001; Prasanna Thati (CAV, 2005)

The ComFoRT Reasoning Framework. - Sagar Chaki; James Ivers; Natasha Sharygina; Kurt C. Wallnau (CAV, 2005)

Dynamic Component Substitutability Analysis. - Natasha Sharygina; Sagar Chaki; Edmund M. Clarke; Nishant Sinha 001 (FM, 2005)

State/Event Software Verification for Branching-Time Specifications. - Sagar Chaki; Edmund M. Clarke; Orna Grumberg; Joël Ouaknine; Natasha Sharygina; Tayssir Touili; Helmut Veith (IFM, 2005)

Parallel Assignments in Software Model Checking. - Murray Stokely; Sagar Chaki; Joël Ouaknine (SVV@ICFEM, 2005)

Concurrent software verification with states, events, and deadlocks. - Sagar Chaki; Edmund M. Clarke; Joël Ouaknine; Natasha Sharygina; Nishant Sinha 001 (Formal Aspects Comput., 2005)

An Iterative Framework for Simulation Conformance. - Sagar Chaki; Edmund M. Clarke; Somesh Jha; Helmut Veith (J. Log. Comput., 2005)

Assume-Guarantee Reasoning for Deadlock. - Sagar Chaki; Nishant Sinha 001 (FMCAD, 2006)

SAT-Based Software Certification. - Sagar Chaki (TACAS, 2006)

Verifying Concurrent Message-Passing C Programs with Recursive Calls. - Sagar Chaki; Edmund M. Clarke; Nicholas Kidd; Thomas W. Reps; Tayssir Touili (TACAS, 2006)

Error explanation with distance metrics. - Alex Groce; Sagar Chaki; Daniel Kroening; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2006)

Model-Driven Construction of Certified Binaries. - Sagar Chaki; James Ivers; Peter Lee 001; Kurt C. Wallnau; Noam Zeilberger (MoDELS, 2007)

Optimized L*-Based Assume-Guarantee Reasoning. - Sagar Chaki; Ofer Strichman (TACAS, 2007)

Verification of evolving software via component substitutability analysis. - Sagar Chaki; Edmund M. Clarke; Natasha Sharygina; Nishant Sinha 001 (Formal Methods Syst. Des., 2008)

Three optimizations for Assume-Guarantee reasoning with L*. - Sagar Chaki; Ofer Strichman (Formal Methods Syst. Des., 2008)

ASPIER: An Automated Framework for Verifying Security Protocol Implementations. - Sagar Chaki; Anupam Datta (CSF, 2009)

Verifying Information Flow Control over Unbounded Processes. - William R. Harris; Nicholas Kidd; Sagar Chaki; Somesh Jha; Thomas W. Reps (FM, 2009)

Decision diagrams for linear arithmetic. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2009)

Towards engineered architecture evolution. - Sagar Chaki; J. Andrés Díaz Pace; David Garlan; Arie Gurfinkel; Ipek Ozkaya (MiSE@ICSE, 2009)

Using Architecturally Significant Requirements for Guiding System Evolution. - Ipek Ozkaya; J. Andrés Díaz Pace; Arie Gurfinkel; Sagar Chaki (CSMR, 2010)

Boxes: A Symbolic Abstract Domain of Boxes. - Arie Gurfinkel; Sagar Chaki (SAS, 2010)

Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size. - Jason Franklin; Sagar Chaki; Anupam Datta; Arvind Seshadri (IEEE Symposium on Security and Privacy, 2010)

Software model checking without source code. - Sagar Chaki; James Ivers (Innov. Syst. Softw. Eng., 2010)

Combining predicate and numeric abstraction for software model checking. - Arie Gurfinkel; Sagar Chaki (Int. J. Softw. Tools Technol. Transf., 2010)

Time-bounded analysis of real-time systems. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2011)

Supervised learning for provenance-similarity of binaries. - Sagar Chaki; Cory F. Cohen; Arie Gurfinkel (KDD, 2011)

Efficient Predicate Abstraction of Program Summaries. - Arie Gurfinkel; Sagar Chaki; Samir Sapra (NASA Formal Methods, 2011)

Automated assume-guarantee reasoning for omega-regular systems and specifications. - Sagar Chaki; Arie Gurfinkel (Innov. Syst. Softw. Eng., 2011)

Non-preemptive Scheduling with History-Dependent Execution Time. - Björn Andersson; Sagar Chaki; Dionisio de Niz; Brian Dougherty; Russell Kegley; Jules White (ECRTS, 2012)

Binary Function Clustering Using Semantic Hashes. - Wesley Jin; Sagar Chaki; Cory F. Cohen; Arie Gurfinkel; Jeffrey Havrilla; Charles Hines; Priya Narasimhan (ICMLA (1), 2012)

Parametric Verification of Address Space Separation. - Jason Franklin; Sagar Chaki; Anupam Datta; Jonathan M. McCune; Amit Vasudevan (POST, 2012)

Regression Verification for Multi-threaded Programs. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (VMCAI, 2012)

Automatic Abstraction in SMT-Based Unbounded Software Model Checking. - Anvesh Komuravelli; Arie Gurfinkel; Sagar Chaki; Edmund M. Clarke (CAV, 2013)

Verifying periodic programs with priority inheritance locks. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2013)

Finding Errors in Python Programs Using Dynamic Symbolic Execution. - Samir Sapra; Marius Minea; Sagar Chaki; Arie Gurfinkel; Edmund M. Clarke (ICTSS, 2013)

Bounded model checking of high-integrity software. - Sagar Chaki (HILT, 2013)

Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework. - Amit Vasudevan; Sagar Chaki; Limin Jia 001; Jonathan M. McCune; James Newsome; Anupam Datta (IEEE Symposium on Security and Privacy, 2013)

Probabilistic Verification of Coordinated Multi-robot Missions. - Sagar Chaki; Joseph Andrew Giampapa (SPIN, 2013)

UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). - Aws Albarghouthi; Arie Gurfinkel; Yi Li 008; Sagar Chaki; Marsha Chechik (TACAS, 2013)

Compositional Sequentialization of Periodic Programs. - Sagar Chaki; Arie Gurfinkel; Soonho Kong; Ofer Strichman (VMCAI, 2013)

Verification across Intellectual Property Boundaries. - Sagar Chaki; Christian Schallhart; Helmut Veith (ACM Trans. Softw. Eng. Methodol., 2013)

Contract-based integration of cyber-physical analyses. - Ivan Ruchkin; Dionisio de Niz; Sagar Chaki; David Garlan (EMSOFT, 2014)

Efficient verification of periodic programs using sequential consistency and snapshots. - Sagar Chaki; Arie Gurfinkel; Nishant Sinha 001 (FMCAD, 2014)

Model-Driven Verifying Compilation of Synchronous Distributed Applications. - Sagar Chaki; James R. Edmondson (MoDELS, 2014)

Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis. - Wesley Jin; Cory F. Cohen; Jeffrey Gennari; Charles Hines; Sagar Chaki; Arie Gurfinkel; Jeffrey Havrilla; Priya Narasimhan (PPREW@POPL, 2014)

Optimizing Robotic Team Performance with Probabilistic Model Checking. - Sagar Chaki; Joseph Andrew Giampapa; David Kyle; John P. Lehoczky (SIMPAR, 2014)

Toward parameterized verification of synchronous distributed applications. - Sagar Chaki; James R. Edmondson (SPIN, 2014)

Eliminating Inter-Domain Vulnerabilities in Cyber-Physical Systems: An Analysis Contracts Approach. - Ivan Ruchkin; Ashwini Rao; Dionisio de Niz; Sagar Chaki; David Garlan (CPS-SPC@CCS, 2015)

High Assurance for Distributed Cyber Physical Systems. - Scott A. Hissam; Sagar Chaki; Gabriel A. Moreno (ECSA Workshops, 2015)

Statistical Model Checking of Distributed Adaptive Real-Time Software. - David Kyle; Jeffery P. Hansen; Sagar Chaki (RV, 2015)

Semantic Importance Sampling for Statistical Model Checking. - Jeffery P. Hansen; Lutz Wrage; Sagar Chaki; Dionisio de Niz; Mark H. Klein 001 (TACAS, 2015)

Scalable Testing of Context-Dependent Policies over Stateful Data Planes with Armstrong. - Seyed Kaveh Fayaz; Yoshiaki Tobioka; Sagar Chaki; Vyas Sekar (CoRR, 2015)

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (Formal Methods Syst. Des., 2015)

Verifying cyber-physical systems by combining software model checking with hybrid systems reachability. - Stanley Bak; Sagar Chaki (EMSOFT, 2016)

BUZZ: Testing Context-Dependent Policies in Stateful Networks. - Seyed Kaveh Fayaz; Tianlong Yu; Yoshiaki Tobioka; Sagar Chaki; Vyas Sekar (NSDI, 2016)

Input Attribution for Statistical Model Checking Using Logistic Regression. - Jeffery P. Hansen; Sagar Chaki; Scott A. Hissam; James R. Edmondson; Gabriel A. Moreno; David Kyle (RV, 2016)

überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. - Amit Vasudevan; Sagar Chaki; Petros Maniatis; Limin Jia 001; Anupam Datta (USENIX Security Symposium, 2016)

Model Checking with Multi-threaded IC3 Portfolios. - Sagar Chaki; Derrick Karimi (VMCAI, 2016)

SMT-based model checking for recursive programs. - Anvesh Komuravelli; Arie Gurfinkel; Sagar Chaki (Formal Methods Syst. Des., 2016)

Decision-Making with Cross-Entropy for Self-Adaptation. - Gabriel A. Moreno; Ofer Strichman; Sagar Chaki; Radislav Vaisman (SEAMS@ICSE, 2017)

Combining Symbolic Runtime Enforcers for Cyber-Physical Systems. - Björn Andersson; Sagar Chaki; Dionisio de Niz (RV, 2017)

Formal Verification of a Timing Enforcer Implementation. - Sagar Chaki; Dionisio de Niz (ACM Trans. Embed. Comput. Syst., 2017)

Have Your PI and Eat it Too: Practical Security on a Low-Cost Ubiquitous Computing Platform. - Amit Vasudevan; Sagar Chaki (EuroS&P, 2018)

BDD-Based Symbolic Model Checking. - Sagar Chaki; Arie Gurfinkel (Handbook of Model Checking, 2018)

High Coverage Concolic Equivalence Checking. - Pritam Roy; Sagar Chaki; Pankaj Chauhan (DATE, 2019)

Achieving high coverage in hardware equivalence checking via concolic verification. - Pritam Roy; Sagar Chaki (Formal Methods Syst. Des., 2022)