[170]
|
NP Satisfiability for Arrays as Powers. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2022.
[ps]
|
[169]
|
Generalized Arrays for Stainless Frames. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2022.
[ps]
|
[168]
|
Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. TACAS. 2022.
[ps]
|
[167]
|
From Verified Scala to STIX File System Embedded Code using Stainless. NASA Formal Methods (NFM). 2022.
[ps]
|
[166]
|
Zippy LL(1) Parsing with Derivatives. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). 2020.
|
[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. ACM SIGPLAN Conf. Programming Language Design and Implementation (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.
|