Viktor Kuncak

Proceedings of the 6th ACM SIGPLAN Symposium on Scala, 2015

Sound reasoning about integral data types with a reusable SMT solver interface.

[BibT_eX]

[DOI]

Régis Blanc

Proceedings of the 6th ACM SIGPLAN Symposium on Scala, 2015

Automating grammar comparison.

[BibT_eX]

[DOI]

Ravichandhran Madhavan

Mikaël Mayer

Sumit Gulwani

Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Programming with enumerable sets of structures.

[BibT_eX]

[DOI]

Ivan Kuraj

Daniel Jackson

Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Synthesizing Java expressions from free-form queries.

[BibT_eX]

[DOI]

Tihomir Gvero

Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Developing Verified Software Using Leon.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Interactive Synthesis Using Free-Form Queries.

[BibT_eX]

[DOI]

Tihomir Gvero

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

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.

[BibT_eX]

[DOI]

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

Deductive Program Repair.

[BibT_eX]

[DOI]

Manos Koukoutos

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

2014

On Numerical Error Propagation with Sensitivity.

[BibT_eX]

[DOI]

CoRR, 2014

Checking Data Structure Properties Orders of Magnitude Faster.

[BibT_eX]

[DOI]

Emmanouil Koukoutos

Proceedings of the Runtime Verification - 5th International Conference, 2014

Sound compilation of reals.

[BibT_eX]

[DOI]

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

Verifying and Synthesizing Software with Recursive Functions - (Invited Contribution).

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

SciFe: Scala framework for efficient enumeration of data structures with invariants.

[BibT_eX]

[DOI]

Ivan Kuraj

Proceedings of the Fifth Annual Scala Workshop, 2014

Symbolic Resource Bound Inference for Functional Programs.

[BibT_eX]

[DOI]

Ravichandhran Madhavan

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Functional synthesis for linear arithmetic and sets.

[BibT_eX]

[DOI]

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

Software verification and graph similarity for automated evaluation of students' assignments.

[BibT_eX]

[DOI]

Milena Vujosevic-Janicic

Mladen Nikolic

Dusan Tosic

Inf. Softw. Technol., 2013

On Integrating Deductive Synthesis and Verification Systems

[BibT_eX]

[DOI]

CoRR, 2013

The Relationship between Craig Interpolation and Recursion-Free Horn Clauses

[BibT_eX]

[DOI]

CoRR, 2013

Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)

[BibT_eX]

[DOI]

CoRR, 2013

Classifying and Solving Horn Clauses for Verification.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Effect Analysis for Programs with Callbacks.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Reductions for Synthesis Procedures.

[BibT_eX]

[DOI]

Swen Jacobs

Proceedings of the Verification, 2013

Automatic synthesis of out-of-core algorithms.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGMOD International Conference on Management of Data, 2013

Executing Specifications Using Synthesis and Constraint Solving.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 4th International Conference, 2013

Complete completion using types and weights.

[BibT_eX]

[DOI]

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

Game programming by demonstration.

[BibT_eX]

[DOI]

Mikaël Mayer

Proceedings of the ACM Symposium on New Ideas in Programming and Reflections on Software, 2013

Synthesis modulo recursive functions.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Interpolation for synthesis on unbounded domains.

[BibT_eX]

[DOI]

Régis Blanc

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

Synthesis of fixed-point programs.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software, 2013

An overview of the Leon verification system: verification by translation to recursive functions.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Scala, 2013

Disjunctive Interpolants for Horn-Clause Verification.

[BibT_eX]

[DOI]

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

2012

Software synthesis procedures.

[BibT_eX]

[DOI]

Commun. ACM, 2012

Abortable Linearizable Modules.

[BibT_eX]

[DOI]

Rachid Guerraoui

Giuliano Losa

Arch. Formal Proofs, 2012

Deciding Functional Lists with Sublist Sets.

[BibT_eX]

[DOI]

Thomas Wies

Marco Muñiz

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System Description.

[BibT_eX]

[DOI]

Milena Vujosevic-Janicic

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Certifying Solutions for Numerical Constraints.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, Third International Conference, 2012

Constraints as control.

[BibT_eX]

[DOI]

Ali Sinan Köksal

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

Speculative linearizability.

[BibT_eX]

[DOI]

Rachid Guerraoui

Giuliano Losa

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

A Verification Toolkit for Numerical Transition Systems - Tool Paper.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

Synthesis for Unbounded Bit-Vector Arithmetic.

[BibT_eX]

[DOI]

Andrej Spielmann

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Accelerating Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2012

2011

Sets with Cardinality Constraints in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Robin Steiger

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

Towards Complete Reasoning about Axiomatic Specifications.

[BibT_eX]

[DOI]

Swen Jacobs

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

Satisfiability Modulo Recursive Programs.

[BibT_eX]

[DOI]

Ali Sinan Köksal

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

Trustworthy numerical computation in Scala.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Interactive Synthesis of Code Snippets.

[BibT_eX]

[DOI]

Tihomir Gvero

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

An Efficient Decision Procedure for Imperative Tree Data Structures.

[BibT_eX]

[DOI]

Thomas Wies

Marco Muñiz

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Scala to the Power of Z3: Integrating SMT and Programming.

[BibT_eX]

[DOI]

Ali Sinan Köksal

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Predicting and preventing inconsistencies in deployed distributed systems.

[BibT_eX]

[DOI]

ACM Trans. Comput. Syst., 2010

Collections, Cardinalities, and Relations.

[BibT_eX]

[DOI]

Kuat Yessenov

Proceedings of the Verification, 2010

Building a Calculus of Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Phantm: PHP analyzer for type mismatch.

[BibT_eX]

[DOI]

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

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - First International Conference, 2010

Decision procedures for algebraic data types with abstractions.

[BibT_eX]

[DOI]

Mirco Dotta

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Complete functional synthesis.

[BibT_eX]

[DOI]

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

Test generation through programming in UDITA.

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Synthesis for regular specifications over unbounded domains.

[BibT_eX]

[DOI]

Jad Hamza

Barbara Jobstmann

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Ordered Sets in the Calculus of Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Comfusy: A Tool for Complete Functional Synthesis.

[BibT_eX]

[DOI]

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

MUNCH - Automated Reasoner for Sets and Multisets.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Opis: reliable distributed systems in OCaml.

[BibT_eX]

[DOI]

Pierre-Évariste Dagand

Dejan Kostic

Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

An integrated proof language for imperative programs.

[BibT_eX]

[DOI]

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

CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, 2009

Simplifying Distributed System Development.

[BibT_eX]

[DOI]

Proceedings of HotOS'09: 12th Workshop on Hot Topics in Operating Systems, 2009

Combining Theories with Shared Set Operations.

[BibT_eX]

[DOI]

Thomas Wies

Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

2008

Decision Procedures for Multisets with Cardinality Constraints.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2008

Runtime Checking for Separation Logic.

[BibT_eX]

[DOI]

Huu Hai Nguyen

Wei-Ngan Chin

Proceedings of the Verification, 2008

Full functional verification of linked data structures.

[BibT_eX]

[DOI]

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

Verifying linked data structure implementations.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE International Symposium on Parallel and Distributed Processing, 2008

Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Linear Arithmetic with Stars.

[BibT_eX]

[DOI]

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

2007

Modular data structure verification.

[BibT_eX]

[DOI]

PhD thesis, 2007

Using First-Order Theorem Provers in the Jahob Data Structure Verification System.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

Runtime Checking for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, 7th International Workshop, 2007

Polynomial Constraints for Sets with Cardinality Bounds.

[BibT_eX]

[DOI]

Bruno Marnette

Proceedings of the Foundations of Software Science and Computational Structures, 2007

Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Modular Pluggable Analyses for Data Structure Consistency.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2006

Deciding Boolean Algebra with Presburger Arithmetic.

[BibT_eX]

[DOI]

Huu Hai Nguyen

J. Autom. Reason., 2006

On Verifying Complex Properties using Symbolic Shape Analysis

[BibT_eX]

[DOI]

CoRR, 2006

Field Constraint Analysis.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2006

An overview of the Jahob analysis system: project goals and current status.

[BibT_eX]

[DOI]

Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

2005

Decision Procedures for Set-Valued Fields.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, 2005

Implications of a Data Structure Consistency Checking System.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Generalized Typestate Checking for Data Structure Consistency.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2005

Relational analysis of algebraic datatypes.

[BibT_eX]

[DOI]

Daniel Jackson

Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

On Algorithms and Complexity for Sets with Cardinality Constraints.

[BibT_eX]

[DOI]

Bruno Marnette

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

Hob: A Tool for Verifying Data Structure Consistency.

[BibT_eX]

[DOI]

Proceedings of the Compiler Construction, 14th International Conference, 2005

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic.

[BibT_eX]

[DOI]

Huu Hai Nguyen

Proceedings of the Automated Deduction, 2005

Crosscutting techniques in program specification and analysis.

[BibT_eX]

[DOI]

Proceedings of the 4th International Conference on Aspect-Oriented Software Development, 2005

2004

Generalized typestate checking using set interfaces and pluggable analyses.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 2004

On computing the fixpoint of a set of boolean equations

[BibT_eX]

[DOI]

K. Rustan M. Leino

CoRR, 2004

On Role Logic

[BibT_eX]

[DOI]

CoRR, 2004

Typestate Checking and Regular Graph Constraints

[BibT_eX]

[DOI]

CoRR, 2004

Roles Are Really Great!

[BibT_eX]

[DOI]

CoRR, 2004

On Spatial Conjunction as Second-Order Logic

[BibT_eX]

[DOI]

CoRR, 2004

On the Theory of Structural Subtyping

[BibT_eX]

[DOI]

CoRR, 2004

The First-Order Theory of Sets with Cardinality Constraints is Decidable

[BibT_eX]

[DOI]

CoRR, 2004

File Refinement.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2004

Binary Search Trees.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2004

Boolean Algebra of Shape Analysis Constraints.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2004

Generalized Records and Spatial Conjunction in Role Logic.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 11th International Symposium, 2004

Verifying a File System Implementation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2004

2003

Existential Heap Abstraction Entailment Is Undecidable.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 10th International Symposium, 2003

Structural Subtyping of Non-Recursive Types is Decidable.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

2002

Numerical Representations as Purely Functional Data Structures: a New Approach.

[BibT_eX]

[DOI]

Mirjana Ivanovic

Informatica, 2002

Role analysis.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

2001

A Language for Role Specifications.

[BibT_eX]

[DOI]

Proceedings of the Languages and Compilers for Parallel Computing, 2001

Confluence of Untyped Lambda Calculus via Simple Types.

[BibT_eX]

[DOI]

Silvia Ghilezan