| [165] | System FR: Formalized Foundations for the Stainless Verifier. Proc. ACM Program. Lang. OOPSLA. 2019. |
| [164] | Minimal Synthesis of String to String Functions from Examples. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2019. |
| [163] | Bidirectional Evaluation with Direct Manipulation. Proc. ACM Program. Lang. OOPSLA, Article 127. 2018. |
| [162] | Towards a Compiler for Reals. ACM Trans. Program. Lang. Syst. (TOPLAS). 2. 2017. |
| [161] | Contract-Based Resource Verification for Higher-order Functions with Memoization. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2017. |
| [160] | Proactive Synthesis of Recursive Tree-to-String Functions from Examples. 31st European Conference on Object-Oriented Programming (ECOOP 2017). 2017. |
| [159] | Refutation-based synthesis in SMT. Formal Methods in System Design (FMSD). 2017. |
| [158] | Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods in System Design (FMSD). 2017. |
| [157] | Translating Scala Programs to Isabelle/HOL (System Description). International Joint Conference on Automated Reasoning (IJCAR). 2016. [ps] |
| [156] | An Update on Deductive Synthesis and Repair in the Leon Tool. 5th Workshop on Synthesis. 2016. |
| [155] | SMT-Based Checking of Predicate-Qualified Types for Scala. Scala Symposium. 2016. |
| [154] | Induction for SMT Solvers. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2015. |
| [153] | Developing Verified Software Using Leon (Invited Contribution). NASA Formal Methods (NFM). 2015. |
| [152] | Interactive Synthesis Using Free-Form Queries (Tool Demonstration). International Conference on Software Engineering (ICSE). 2015. |
| [151] | Sound Reasoning about Integral Data Types with a Reusable SMT Solver Interface. Scala Symposium. 2015. |
| [150] | Counter-Example Complete Verification for Higher-Order Functions. Scala Symposium. 2015. |
| [149] | Counterexample Guided Quantifier Instantiation for Synthesis in SMT. Computer-Aided Verification (CAV). 2015. |
| [148] | Deductive Program Repair. Computer-Aided Verification (CAV). 2015. |
| [147] | Automating Grammar Comparison. OOPSLA. 2015. |
| [146] | Synthesizing Java Expressions from Free-Form Queries. OOPSLA. 2015. |
| [145] | Programming with Enumerable Sets of Structures. OOPSLA. 2015. |
| [144] | Sound Compilation of Reals. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2014. |
| [143] | Symbolic Resource Bound Inference for Functional Programs. Computer Aided Verification (CAV). 2014. [ps] |
| [142] | Verifying and Synthesizing Software with Recursive Functions (Invited Contribution). 41st International Colloquium on Automata, Languages, and Programming (ICALP). 2014. [ps] |
| [141] | Checking Data Structure Properties Orders of Magnitude Faster. Runtime Verification (RV). 2014. |
| [140] | SciFe: Scala Framework for Efficient Enumeration of Data Structures with Invariants. Scala Workshop. 2014. |
| [139] | Synthesizing Functions from Relations in Leon (Invited Contribution). Logic-Based Program Synthesis and Transformation (LOPSTR). 2014. |
| [138] | On Synthesizing Code from Free-Form Queries. EPFL Technical Report EPFL-REPORT-201606. 2014. |
| [137] | On Induction for SMT Solvers. EPFL Technical Report EPFL-REPORT-201755. 2014. |
| [136] | On Template-Based Inference of Rich Invariants in Leon. EPFL Technical Report EPFL-REPORT-190578. 2013. |
| [135] | Reductions for Synthesis Procedures. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2013. |
| [134] | Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. Information and Software Technology. 2013. |
| [133] | Complete Completion using Types and Weights. PLDI. 2013. |
| [132] | Disjunctive Interpolants for Horn-Clause Verification. Computer Aided Verification (CAV). 2013. |
| [131] | On Integrating Deductive Synthesis and Verification Systems. EPFL Technical Report EPFL-REPORT-186043. 2013. |
| [130] | On Verification by Translation to Recursive Functions. EPFL Technical Report EPFL-REPORT-186233. 2013. |
| [129] | Automatic Synthesis of Out-of-Core Algorithms. SIGMOD. 2013. [ps] |
| [128] | An Overview of the Leon Verification System: Verification by Translation to Recursive Functions. Scala Workshop. 2013. [ps] |
| [127] | Executing Specifications using Synthesis and Constraint Solving (Invited Talk). Runtime Verification (RV). 2013. [ps] |
| [126] | Classifying and Solving Horn Clauses for Verification. Fifth Working Conference on Verified Software: Theories, Tools and Experiments. 2013. |
| [125] | Effect Analysis for Programs with Callbacks. Fifth Working Conference on Verified Software: Theories, Tools and Experiments. 2013. |
| [124] | Synthesis of Fixed-Point Programs. Embedded Software (EMSOFT). 2013. [ps] |
| [123] | Interpolation for Synthesis on Unbounded Domains. Formal Methods in Computer-Aided Design (FMCAD). 2013. |
| [122] | Game Programming by Demonstration. SPLASH Onward!. 2013. |
| [121] | Synthesis Modulo Recursive Functions. OOPSLA. 2013. [ps] |
| [120] | Constraints as Control. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2012. [ps] |
| [119] | Development and Evaluation of LAV: an SMT-Based Error Finding Platform. Verified Software: Theories, Tools and Experiments (VSTTE). 2012. [ps] |
| [118] | Deciding Functional Lists with Sublist Sets. Verified Software: Theories, Tools and Experiments (VSTTE). 2012. [ps] |
| [117] | Functional Synthesis for Linear Arithmetic and Sets. Software Tools for Technology Transfer (STTT). TBD. 2012. |
| [116] | Software Synthesis Procedures. Communications of the ACM. 2012. [ps] |
| [115] | Speculative Linearizability. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2012. [ps] |
| [114] | Synthesis for Unbounded Bitvector Arithmetic. International Joint Conference on Automated Reasoning (IJCAR). 2012. |
| [113] | A Verification Toolkit for Numerical Transition Systems (Tool Paper). 16th International Symposium on Formal Methods (FM). 2012. |
| [112] | Accelerating Interpolants. Automated Technology for Verification and Analysis (ATVA). 2012. [ps] |
| [111] | Certifying Solutions for Numerical Constraints. Runtime Verification (RV). 2012. |
| [110] | Towards Complete Reasoning about Axiomatic Specifications. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2011. [ps] |
| [109] | Sets with Cardinality Constraints in Satisfiability Modulo Theories. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2011. [ps] |
| [108] | Interactive Synthesis of Code Snippets. Computer Aided Verification (CAV) Tool Demo. 2011. |
| [107] | Scala to the Power of Z3: Integrating SMT and Programming. Computer-Aideded Deduction (CADE) Tool Demo. 2011. |
| [106] | An Efficient Decision Procedure for Imperative Tree Data Structures. Computer-Aideded Deduction (CADE). 2011. |
| [105] | Satisfiability Modulo Recursive Programs. Static Analysis Symposium (SAS). 2011. [ps] |
| [104] | Trustworthy Numerical Computation in Scala. OOPSLA. 2011. [ps] |
| [103] | On Locality of One-Variable Axioms and Piecewise Combinations. EPFL Technical Report EPFL-REPORT-148180. 2010. [ps] |
| [102] | On Deciding Functional Lists with Sublist Sets. EPFL Technical Report EPFL-REPORT-148361. 2010. [ps] |
| [101] | Decision Procedures for Algebraic Data Types with Abstractions. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2010. [ps] |
| [100] | Collections, Cardinalities, and Relations. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2010. [ps] |
| [99] | Building a Calculus of Data Structures (invited paper). Verification, Model Checking, and Abstract Interpretation (VMCAI). 2010. [ps] |
| [98] | Predicting and Preventing Inconsistencies in Deployed Distributed Systems. ACM Transactions on Computer Systems. 1. 2010. [ps] |
| [97] | Test Generation through Programming in UDITA. International Conference on Software Engineering (ICSE). 2010. [ps] |
| [96] | On Decision Procedures for Ordered Collections. EPFL Technical Report LARA-REPORT-2010-001. 2010. [ps] |
| [95] | Complete Functional Synthesis. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2010. [ps] |
| [94] | Comfusy: Complete Functional Synthesis (Tool Presentation). CAV. 2010. [ps] |
| [93] | MUNCH - Automated Reasoner for Sets and Multisets (System Description). IJCAR. 2010. [ps] |
| [92] | Ordered Sets in the Calculus of Data Structures (Invited Paper). CSL. 2010. [ps] |
| [91] | Synthesis for Regular Specifications over Unbounded Domains. FMCAD. 2010. [ps] |
| [90] | Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. International Conference on Runtime Verification. 2010. [ps] |
| [89] | Phantm: PHP Analyzer for Type Mismatch (Research Demonstration). ACM SIGSOFT Conference on Foundations of Software Engineering (FSE). 2010. [ps] |
| [88] | On Rigorous Numerical Computation as a Scala Library. EPFL Technical Report EPFL-REPORT-158754. 2010. |
| [87] | On Satisfiability Modulo Computable Functions. EPFL Technical Report EPFL-REPORT. 2010. |
| [86] | On Test Generation through Programming in UDITA. EPFL, IC Technical Report LARA-REPORT-2009-05. 2009. [ps] |
| [85] | On Decision Procedures for Collections, Cardinalities, and Relations. EPFL Technical Report LARA-REPORT-2009-004. 2009. [ps] |
| [84] | On Decision Procedures for Algebraic Data Types with Abstractions. EPFL Technical Report LARA-REPORT-2009-003. 2009. [ps] |
| [83] | On Combining Theories with Shared Set Operations. EPFL Technical Report LARA-REPORT-2009-002. 2009. |
| [82] | On Set-Driven Combination of Logics and Verifiers. EPFL Technical Report LARA-REPORT-2009-001. 2009. |
| [81] | Opis: Reliable Distributed Systems in OCaml. ACM SIGPLAN TLDI. 2009. |
| [80] | CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. 6th USENIX Symp. Networked Systems Design and Implementation (NSDI '09). 2009. [ps] |
| [79] | Simplifying Distributed System Development. EPFL Technical Report NSL-REPORT-2009-001. 2009. |
| [78] | An Integrated Proof Language for Imperative Programs. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2009. [ps] |
| [77] | Simplifying Distributed System Development. 12th Workshop on Hot Topics in Operating Systems. 2009. [ps] |
| [76] | Combining Theories with Shared Set Operations. FroCoS: Frontiers in Combining Systems. 2009. [ps] |
| [75] | On Complete Functional Synthesis. EPFL Technical Report LARA-REPORT-2009-006. 2009. [ps] |
| [74] | Constraint Solving for Software Reliability and Text Analysis (Research Plan). EPFL Technical Report LARA-REPORT-2008-007. 2008. |
| [73] | CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. EPFL-IC-LARA Technical Report LARA-REPORT-2008-006. 2008. |
| [72] | Runtime Checking for Separation Logic. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 2008. |
| [71] | Decision Procedures for Multisets with Cardinality Constraints. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 2008. [ps] |
| [70] | On Static Analysis for Expressive Pattern Matching. EPFL Technical Report LARA-REPORT-2008-004. 2008. [ps] |
| [69] | On Linear Arithmetic with Stars. EPFL Technical Report LARA-REPORT-2008-005. 2008. [ps] |
| [68] | Full Functional Verification of Linked Data Structures. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2008. [ps] |
| [67] | Linear Arithmetic with Stars. Computed-Aided Verification (CAV). 2008. [ps] |
| [66] | Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars. Computer Science Logic (CSL). 2008. [ps] |
| [65] | Opis: Reliable Distributed Systems in OCaml. EPFL-IC-NSL Technical Report NSL-REPORT-2008-001. 2008. |
| [64] | On Delayed Choice Execution for Falsification. EPFL, IC Technical Report LARA-REPORT-2008-08. 2008. |
| [63] | Using First-Order Theorem Provers in the Jahob Data Structure Verification System. Verification, Model Checking and Abstract Interpretation. 2007. [ps] |
| [62] | Polynomial Constraints for Sets with Cardinality Bounds. Foundations of Software Science and Computation Structures (FOSSACS). 2007. [ps] |
| [61] | Modular Data Structure Verification. PhD Thesis, EECS Department, Massachusetts Institute of Technology. 2007. [ps] |
| [60] | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete. MIT CSAIL Technical Report MIT-CSAIL-TR-2007-001. 2007. [ps] |
| [59] | Runtime Checking for Program Verification. Workshop on Runtime Verification. 2007. |
| [58] | Verifying Complex Properties using Symbolic Shape Analysis. Workshop on Heap Abstraction and Verification (collocated with ETAPS). 2007. [ps] |
| [57] | Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. Conference on Automateded Deduction (CADE-21). 2007. [ps] |
| [56] | Runtime Checking for Separation Logic. EPFL Technical Report LARA-REPORT-2007-003. 2007. |
| [55] | Decision Procedures for Multisets with Cardinality Constraints. EPFL Technical Report LARA-REPORT-2007-002. 2007. |
| [54] | Modular Pluggable Analyses for Data Structure Consistency. IEEE Transactions on Software Engineering (TSE). 12. 2006. [ps] |
| [53] | On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System. MIT Technical Report MIT-CSAIL-TR-2006-072. 2006. [ps] |
| [52] | Field Constraint Analysis. Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation. 2006. [ps] |
| [51] | An overview of the Jahob analysis system: Project Goals and Current Status. NSF Next Generation Software Workshop. 2006. [ps] |
| [50] | Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning. 3. 2006. [ps] |
| [49] | On Verifying Complex Properties using Symbolic Shape Analysis. Max-Planck Institute for Computer Science Technical Report MPI-I-2006-2-1. 2006. |
| [48] | On Field Constraint Analysis. MIT CSAIL Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010. 2005. [ps] |
| [47] | Implications of a Data Structure Consistency Checking System. International conference on Verified Software: Theories, Tools, Experiments (VSTTE, IFIP Working Group 2.3 Conference). 2005. [ps] |
| [46] | On Algorithms and Complexity for Sets with Cardinality Constraints. MIT CSAIL Technical Report 2005. [ps] |
| [45] | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. 20th International Conference on Automated Deduction, CADE-20. 2005. [ps] |
| [44] | Hob: A Tool for Verifying Data Structure Consistency. 14th International Conference on Compiler Construction (tool demo). 2005. [ps] |
| [43] | On Relational Analysis of Algebraic Datatypes. MIT Technical Report 985. 2005. [ps] |
| [42] | Cross-Cutting Techniques in Program Specification and Analysis. 4th International Conference on Aspect-Oriented Software Development. 2005. [ps] |
| [41] | Generalized Typestate Checking for Data Structure Consistency. Verification, Model Checking and Abstract Interpretation. 2005. [ps] |
| [40] | Decision Procedures for Set-Valued Fields. Electr. Notes Theor. Comput. Sci.; Proc. Abstract Interpretation of Object-Oriented Languages. 2005. [ps] |
| [39] | Relational Analysis of Algebraic Datatypes. 10th European Soft. Eng. Conf. (ESEC) and 13th Symp. Foundations of Software Engineering (FSE). 2005. [ps] |
| [38] | File Refinement. The Archive of Formal Proofs. 2004. |
| [37] | Combining Theorem proving with Static Analysis for Data Structure Consistency. International Workshop on Software Verification and Validation. 2004. [ps] |
| [36] | On Decision Procedures for Set-Valued Fields. MIT CSAIL Technical Report 975. 2004. [ps] |
| [35] | On Spatial Conjunction as Second-Order Logic. MIT CSAIL Technical Report 970. 2004. [ps] |
| [34] | Modular Pluggable Analyses for Data Structure Consistency. Monterey Workshop on Software Engineering Tools: Compatibility and Integration. 2004. |
| [33] | On Our Experience with Modular Pluggable Analyses. MIT CSAIL Technical Report 965. 2004. [ps] |
| [32] | Generalized Records and Spatial Conjunction in Role Logic. International Static Analysis Symposium. 2004. [ps] |
| [31] | The First-Order Theory of Sets with Cardinality Constraints is Decidable. MIT CSAIL Technical Report 958. 2004. [ps] |
| [30] | On Verifying a File System Implementation. MIT CSAIL Technical Report 946. 2004. [ps] |
| [29] | On Generalized Records and Spatial Conjunction in Role Logic. MIT CSAIL Technical Report 942. 2004. [ps] |
| [28] | Binary Search Trees. The Archive of Formal Proofs. 2004. |
| [27] | Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses. SIGPLAN Notices. 2004. [ps] |
| [26] | Boolean Algebra of Shape Analysis Constraints. Verification, Model Checking and Abstract Interpretation. 2004. [ps] |
| [25] | Verifying a File System Implementation. Sixth International Conference on Formal Engineering Methods. 2004. [ps] |
| [24] | On Modular Pluggable Analyses Using Set Interfaces. MIT CSAIL Technical Report 933. 2003. [ps] |
| [23] | On computing the fixpoint of a set of boolean equations. Microsoft Research Technical Report MSR-TR-2003-08. 2003. [ps] |
| [22] | On the Boolean Algebra of Shape Analysis Constraints. MIT CSAIL Technical Report 2003. [ps] |
| [21] | Existential Heap Abstraction Entailment is Undecidable. 10th Annual International Static Analysis Symposium. 2003. [ps] |
| [20] | In-Place Refinement for Effect Checking. Workshop on Automated Verification of Infinite-State Systems. 2003. [ps] |
| [19] | On the Theory of Structural Subtyping. MIT LCS Technical Report 879. 2003. [ps] |
| [18] | Structural Subtyping of Non-Recursive Types is Decidable. Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS). 2003. [ps] |
| [17] | On Role Logic. MIT CSAIL Technical Report 925. 2003. [ps] |
| [16] | Numerical Representations as Purely Functional Data Structures: A New Approach. INFORMATICA, Institute of Mathematics and Informatics, Vilnius. 2. 2002. |
| [15] | Role Analysis. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2002. [ps] |
| [14] | Typestate Checking and Regular Graph Constraints. MIT LCS Technical Report 863. 2002. [ps] |
| [13] | Confluence of untyped lambda calculus via simple types. Proceedings of the 7th Italian Conference on Theoretical Computer Science, ICTCS 2001. 2001. |
| [12] | Reducibility method for termination properties of typed lambda terms. Fifth International Workshop on Termination. 2001. |
| [11] | Types and confluence in lambda calculus. 3rd Panhellenic Logic Symposium. 2001. |
| [10] | Object Models, Heaps, and Interpretations. MIT LCS Technical Report 816. 2001. [ps] |
| [9] | A Language for Role Specifications. Workshop on Languages and Compilers for Parallel Computing. 2001. [ps] |
| [8] | Roles are really great!. MIT LCS Technical Report 822. 2001. [ps] |
| [7] | Designing an Algorithm for Role Analysis. Master's Thesis, MIT LCS. 2001. [ps] |
| [6] | Modular Language Specifications in Haskell. Theoretical Aspects of Computer Science with practical application. 2000. [ps] |
| [5] | Reducibility Method in Simply Typed Lambda Calculus. XIV Conference on Applied Mathematics "PRIM", Palić. 2000. |
| [4] | Numerical Representations as Purely Functional Data Structures. XIV Conference on Applied Mathematics "PRIM", Palić. 2000. |
| [3] | Modular Interpreters in Haskell. B.Sc. Thesis, University of Novi Sad. 2000. [ps] |
| [2] | Developing a Multigrid Solver for Standing Wave Equation. Proceedings of the 28th Dr. Bessie F. Lawrence International Summer Science Institute Participants, Weizmann Institute of Science. 1996. [ps] |
| [1] | PLS: Programming Language for Simulations. Proceedings of the Petnica Science Center Seminar '93. 1993. |