Azadeh Farzan

Dominik Klumpp

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

Ultimate GemCutter SV-COMP 2022 Competition Contribution.

[BibT_eX]

[DOI]

Dataset, November, 2021

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2021

Phased synthesis of divide and conquer programs.

[BibT_eX]

[DOI]

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

Counterexample-Guided Partial Bounding for Recursive Function Synthesis.

[BibT_eX]

[DOI]

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

2020

Reductions for safety proofs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Root Causing Linearizability Violations.

[BibT_eX]

[DOI]

Berk Çirisci

Constantin Enea

Suha Orhun Mutluergil

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Reductions for Safety Proofs (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2019

Reductions for Automated Hypersafety Verification.

[BibT_eX]

[DOI]

CoRR, 2019

Modular Synthesis of Divide-and-Conquer Parallelism for Nested Loops (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2019

Modular divide-and-conquer parallelization of nested loops.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Automated Hypersafety Verification.

[BibT_eX]

[DOI]

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

2018

Strategy synthesis for linear arithmetic games.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

2017

Automated Synthesis of Divide and Conquer Parallelism.

[BibT_eX]

[DOI]

CoRR, 2017

Synthesis of divide and conquer parallelism for loops.

[BibT_eX]

[DOI]

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

On Atomicity in Presence of Non-atomic Writes.

[BibT_eX]

[DOI]

Constantin Enea

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution.

[BibT_eX]

[DOI]

Andreas Holzer

Helmut Veith

Proceedings of the 8th IEEE International Conference on Software Testing, 2015

Compositional Recurrence Analysis.

[BibT_eX]

[DOI]

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

2014

Generating effective tests for concurrent programs via AI automated planning techniques.

[BibT_eX]

[DOI]

Niloofar Razavi

Sheila A. McIlraith

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

Concolic Testing of Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik, 25. Februar, 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

Con2colic testing.

[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

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

2012

Predicting null-pointer dereferences in concurrent programs.

[BibT_eX]

[DOI]

Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 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

Bounded-Interference Sequentialization for Testing Concurrent Programs.

[BibT_eX]

[DOI]

Niloofar Razavi

Andreas Holzer

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, 2012

2010

PENELOPE: weaving threads to expose atomicity violations.

[BibT_eX]

[DOI]

Francesco Sorrentino

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Compositional Bitvector Analysis for Concurrent Programs with Nested Locks.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 17th International Symposium, 2010

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Automated Assume-Guarantee Reasoning through Implicit Learning.

[BibT_eX]

[DOI]

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

2009

The Complexity of Predicting Atomicity Violations.

[BibT_eX]

[DOI]

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

Learning Minimal Separating DFA's for Compositional Verification.

[BibT_eX]

[DOI]

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

Meta-analysis for Atomicity Violations under Nested Locking.

[BibT_eX]

[DOI]

Francesco Sorrentino

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

2008

Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages.

[BibT_eX]

[DOI]

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

Monitoring Atomicity in Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Static and Dynamic Formal Analysis of Concurrent Systems and Languages: A Semantics-Based Approach

[BibT_eX]

[DOI]

PhD thesis, 2007

Causal Dataflow Analysis for Concurrent Programs.

[BibT_eX]

[DOI]

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

Some Tools.

[BibT_eX]

[DOI]

Proceedings of the All About Maude, 2007

2006

Partial Order Reduction for Rewriting Semantics of Programming Languages.

[BibT_eX]

[DOI]

José Meseguer

Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, 2006

Causal Atomicity.

[BibT_eX]

[DOI]

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

State Space Reduction of Rewrite Theories Using Invisible Transitions.

[BibT_eX]

[DOI]

José Meseguer

Proceedings of the Algebraic Methodology and Software Technology, 2006

2004

Formal Analysis of Java Programs in JavaFAN.

[BibT_eX]

[DOI]

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

Formal JVM Code Analysis in JavaFAN.

[BibT_eX]

[DOI]