Zachary Kincaid

Proc. ACM Program. Lang., January, 2024

Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials.

[BibT_eX]

[DOI]

Nikhil Pimpalkhare

Proc. ACM Program. Lang., 2024

Relational Network Verification.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGCOMM 2024 Conference, 2024

Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability.

[BibT_eX]

[DOI]

Nikhil Pimpalkhare

Proceedings of the Reachability Problems - 18th International Conference, 2024

Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement.

[BibT_eX]

[DOI]

Charlie Murphy

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic.

[BibT_eX]

[DOI]

Nicolas Koh

Proc. ACM Program. Lang., January, 2023

Optimal Symbolic Bound Synthesis.

[BibT_eX]

[DOI]

CoRR, 2023

2021

Termination analysis without the tears.

[BibT_eX]

[DOI]

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Reflections on Termination of Linear Loops.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Algebraic Program Analysis.

[BibT_eX]

[DOI]

Thomas W. Reps

John Cyphert

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Templates and recurrences: better together.

[BibT_eX]

[DOI]

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

2019

Closed forms for numerical loops.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Refinement of path expressions for static analysis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Loop Summarization with Rational Vector Addition Systems (extended version).

[BibT_eX]

[DOI]

Jake Silverman

CoRR, 2019

A Practical Algorithm for Structure Embedding.

[BibT_eX]

[DOI]

Charlie Murphy

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

Loop Summarization with Rational Vector Addition Systems.

[BibT_eX]

[DOI]

Jake Silverman

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Non-linear reasoning for invariant synthesis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Strategy synthesis for linear arithmetic games.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

A Symbolic Decision Procedure for Symbolic Alternating Finite Automata.

[BibT_eX]

[DOI]

Loris D'Antoni

Fang Wang

Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, 2018

Numerical Invariants via Abstract Machines.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 25th International Symposium, 2018

2017

Parallel Proofs for Parallel Programs.

[BibT_eX]

[DOI]

PhD thesis, 2017

Compositional recurrence analysis revisited.

[BibT_eX]

[DOI]

Jason Breck

Ashkan Forouhi Boroujeni

Thomas W. Reps

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 28th International Conference on Concurrency Theory, 2017

2016

Proving Liveness of Parameterized Programs.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Linear Arithmetic Satisfiability via Strategy Improvement.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

2015

Compositional Invariant Generation via Linear Recurrence Analysis.

[BibT_eX]

[DOI]

CoRR, 2015

Proof Spaces for Unbounded Parallelism.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Automated Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2015

Compositional Recurrence Analysis.

[BibT_eX]

[DOI]

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

Spatial Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

2014

Symbolic optimization with SMT solvers.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Proofs that count.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Consistency analysis of decision-making programs.

[BibT_eX]

[DOI]

Swarat Chaudhuri

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

An Algebraic Framework for Compositional Program Analysis.

[BibT_eX]

[DOI]

CoRR, 2013

Inductive data flow graphs.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Duet: Static Analysis for Unbounded Parallelism.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Recursive Program Synthesis.

[BibT_eX]

[DOI]

Aws Albarghouthi

Sumit Gulwani

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Verification of parameterized concurrent programs by modular reasoning about data and control.

[BibT_eX]

[DOI]

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

2010

Compositional Bitvector Analysis for Concurrent Programs with Nested Locks.

[BibT_eX]

[DOI]