| [93] | Complete Functional Synthesis. PLDI. 2010. [ bib ] |
| [92] | On Decision Procedures for Ordered Collections. EPFL Technical Report LARA-REPORT-2010-001. 2010. [ps] [ bib | Abstract ] |
| [91] | Test Generation through Programming in UDITA. International Conference on Software Engineering (ICSE). 2010. [ps] [ bib | http | Abstract ] |
| [90] | Predicting and Preventing Inconsistencies in Deployed Distributed Systems. ACM Transactions on Computer Systems. 2010. [ps] [ bib | Abstract ] |
| [89] | Building a Calculus of Data Structures. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2010. [ps] [ bib | Abstract ] |
| [88] | Collections, Cardinalities, and Relations. Verification, Model Checking, and Abstract Interpretation (VMCAI). 2010. [ps] [ bib ] |
| [87] | On Complete Functional Synthesis. EPFL Technical Report LARA-REPORT-2009-006. 2009. [ps] [ bib ] |
| [86] | Decision Procedures for Algebraic Data Types with Abstractions. 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). 2010. [ps] [ bib ] |
| [85] | On Test Generation through Programming in UDITA. EPFL, IC Technical Report LARA-REPORT-2009-05. 2009. [ps] [ bib | http | Abstract ] |
| [84] | On Decision Procedures for Collections, Cardinalities, and Relations. EPFL Technical Report LARA-REPORT-2009-004. 2009. [ps] [ bib | Abstract ] |
| [83] | On Decision Procedures for Algebraic Data Types with Abstractions. EPFL Technical Report LARA-REPORT-2009-003. 2009. [ps] [ bib | Abstract ] |
| [82] | Combining Theories with Shared Set Operations. FroCoS: Frontiers in Combining Systems. 2009. [ps] [ bib ] |
| [81] | On Combining Theories with Shared Set Operations. EPFL Technical Report LARA-REPORT-2009-002. 2009. [ bib ] |
| [80] | Simplifying Distributed System Development. 12th Workshop on Hot Topics in Operating Systems. 2009. [ps] [ bib | Abstract ] |
| [79] | An Integrated Proof Language for Imperative Programs. ACM Conf. Programming Language Design and Implementation (PLDI). 2009. [ps] [ bib ] |
| [78] | On Set-Driven Combination of Logics and Verifiers. EPFL Technical Report LARA-REPORT-2009-001. 2009. [ bib | Abstract ] |
| [77] | Simplifying Distributed System Development. EPFL Technical Report NSL-REPORT-2009-001. 2009. [ bib | Abstract ] |
| [76] | CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. 6th USENIX Symp. Networked Systems Design and Implementation (NSDI '09). 2009. [ps] [ bib | .html | Abstract ] |
| [75] | Opis: Reliable Distributed Systems in OCaml. ACM SIGPLAN TLDI. 2009. [ bib | Abstract ] |
| [74] | On Delayed Choice Execution for Falsification. EPFL, IC Technical Report LARA-REPORT-2008-08. 2008. [ bib ] |
| [73] | Constraint Solving for Software Reliability and Text Analysis (Research Plan). EPFL Technical Report LARA-REPORT-2008-007. 2008. [ bib | Abstract ] |
| [72] | Opis: Reliable Distributed Systems in OCaml. EPFL-IC-NSL Technical Report NSL-REPORT-2008-001. 2008. [ bib | Abstract ] |
| [71] | CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems. EPFL-IC-LARA Technical Report LARA-REPORT-2008-006. 2008. [ bib | Abstract ] |
| [70] | Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars. Computer Science Logic (CSL). 2008. [ps] [ bib | Abstract ] |
| [69] | Linear Arithmetic with Stars. Computed-Aided Verification (CAV). 2008. [ps] [ bib | Abstract ] |
| [68] | Full Functional Verification of Linked Data Structures. ACM Conf. Programming Language Design and Implementation (PLDI). 2008. [ps] [ bib | Abstract ] |
| [67] | On Linear Arithmetic with Stars. EPFL Technical Report LARA-REPORT-2008-005. 2008. [ps] [ bib | Abstract ] |
| [66] | On Static Analysis for Expressive Pattern Matching. EPFL Technical Report LARA-REPORT-2008-004. 2008. [ps] [ bib | Abstract ] |
| [65] | Decision Procedures for Multisets with Cardinality Constraints. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 2008. [ps] [ bib | Abstract ] |
| [64] | Runtime Checking for Separation Logic. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 2008. [ bib | Abstract ] |
| [63] | Decision Procedures for Multisets with Cardinality Constraints. EPFL Technical Report LARA-REPORT-2007-002. 2007. [ bib | Abstract ] |
| [62] | Runtime Checking for Separation Logic. EPFL Technical Report LARA-REPORT-2007-003. 2007. [ bib | Abstract ] |
| [61] | Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. Conference on Automateded Deduction (CADE-21). 2007. [ps] [ bib | Abstract ] |
| [60] | Polynomial Constraints for Sets with Cardinality Bounds. Foundations of Software Science and Computation Structures (FOSSACS). 2007. [ps] [ bib | Abstract ] |
| [59] | Verifying Complex Properties using Symbolic Shape Analysis. Workshop on Heap Abstraction and Verification (collocated with ETAPS). 2007. [ps] [ bib ] |
| [58] | Runtime Checking for Program Verification. Workshop on Runtime Verification. 2007. [ bib | Abstract ] |
| [57] | Modular Data Structure Verification. PhD Thesis, EECS Department, Massachusetts Institute of Technology. 2007. [ps] [ bib | http | Abstract ] |
| [56] | Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete. MIT CSAIL Technical Report MIT-CSAIL-TR-2007-001. 2007. [ps] [ bib | http | Abstract ] |
| [55] | Using First-Order Theorem Provers in the Jahob Data Structure Verification System. Verification, Model Checking and Abstract Interpretation. 2007. [ps] [ bib | Abstract ] |
| [54] | On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System. MIT Technical Report MIT-CSAIL-TR-2006-072. 2006. [ps] [ bib | http | Abstract ] |
| [53] | Modular Pluggable Analyses for Data Structure Consistency. IEEE Transactions on Software Engineering (TSE). 2006. [ps] [ bib | http | Abstract ] |
| [52] | On Verifying Complex Properties using Symbolic Shape Analysis. Max-Planck Institute for Computer Science Technical Report MPI-I-2006-2-1. 2006. [ bib | http | Abstract ] |
| [51] | Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning. 2006. [ps] [ bib | http | Abstract ] |
| [50] | An overview of the Jahob analysis system: Project Goals and Current Status. NSF Next Generation Software Workshop. 2006. [ps] [ bib | Abstract ] |
| [49] | Field Constraint Analysis. Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation. 2006. [ps] [ bib | Abstract ] |
| [48] | On Field Constraint Analysis. MIT CSAIL Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010. 2005. [ps] [ bib | Abstract ] |
| [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] [ bib | Abstract ] |
| [46] | Relational Analysis of Algebraic Datatypes. 10th European Soft. Eng. Conf. (ESEC) and 13th Symp. Foundations of Software Engineering (FSE). 2005. [ps] [ bib | Abstract ] |
| [45] | On Algorithms and Complexity for Sets with Cardinality Constraints. MIT CSAIL Technical Report 2005. [ps] [ bib | http | Abstract ] |
| [44] | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. 20th International Conference on Automated Deduction, CADE-20. 2005. [ps] [ bib | Abstract ] |
| [43] | On Relational Analysis of Algebraic Datatypes. MIT Technical Report 985. 2005. [ps] [ bib | Abstract ] |
| [42] | Hob: A Tool for Verifying Data Structure Consistency. 14th International Conference on Compiler Construction (tool demo). 2005. [ps] [ bib | Abstract ] |
| [41] | Cross-Cutting Techniques in Program Specification and Analysis. 4th International Conference on Aspect-Oriented Software Development. 2005. [ps] [ bib | Abstract ] |
| [40] | Decision Procedures for Set-Valued Fields. Electr. Notes Theor. Comput. Sci.; Proc. Abstract Interpretation of Object-Oriented Languages. 2005. [ps] [ bib | Abstract ] |
| [39] | Generalized Typestate Checking for Data Structure Consistency. Verification, Model Checking and Abstract Interpretation. 2005. [ps] [ bib | Abstract ] |
| [38] | File Refinement. The Archive of Formal Proofs. 2004. [ bib | http ] |
| [37] | Binary Search Trees. The Archive of Formal Proofs. 2004. [ bib | http ] |
| [36] | Modular Pluggable Analyses for Data Structure Consistency. Monterey Workshop on Software Engineering Tools: Compatibility and Integration. 2004. [ bib ] |
| [35] | On Decision Procedures for Set-Valued Fields. MIT CSAIL Technical Report 975. 2004. [ps] [ bib | Abstract ] |
| [34] | Combining Theorem proving with Static Analysis for Data Structure Consistency. International Workshop on Software Verification and Validation. 2004. [ps] [ bib | Abstract ] |
| [33] | On Spatial Conjunction as Second-Order Logic. MIT CSAIL Technical Report 970. 2004. [ps] [ bib | http | Abstract ] |
| [32] | On Our Experience with Modular Pluggable Analyses. MIT CSAIL Technical Report 965. 2004. [ps] [ bib | Abstract ] |
| [31] | The First-Order Theory of Sets with Cardinality Constraints is Decidable. MIT CSAIL Technical Report 958. 2004. [ps] [ bib | http | Abstract ] |
| [30] | Verifying a File System Implementation. Sixth International Conference on Formal Engineering Methods. 2004. [ps] [ bib | Abstract ] |
| [29] | Generalized Records and Spatial Conjunction in Role Logic. International Static Analysis Symposium. 2004. [ps] [ bib | Abstract ] |
| [28] | On Generalized Records and Spatial Conjunction in Role Logic. MIT CSAIL Technical Report 942. 2004. [ps] [ bib | http | Abstract ] |
| [27] | On Verifying a File System Implementation. MIT CSAIL Technical Report 946. 2004. [ps] [ bib | Abstract ] |
| [26] | Boolean Algebra of Shape Analysis Constraints. Verification, Model Checking and Abstract Interpretation. 2004. [ps] [ bib | Abstract ] |
| [25] | On computing the fixpoint of a set of boolean equations. Microsoft Research Technical Report MSR-TR-2003-08. 2003. [ps] [ bib | http | Abstract ] |
| [24] | On Modular Pluggable Analyses Using Set Interfaces. MIT CSAIL Technical Report 933. 2003. [ps] [ bib | Abstract ] |
| [23] | Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses. SIGPLAN Notices. 2004. [ps] [ bib | Abstract ] |
| [22] | On Role Logic. MIT CSAIL Technical Report 925. 2003. [ps] [ bib | http | Abstract ] |
| [21] | On the Boolean Algebra of Shape Analysis Constraints. MIT CSAIL Technical Report 2003. [ps] [ bib | Abstract ] |
| [20] | Structural Subtyping of Non-Recursive Types is Decidable. Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS). 2003. [ps] [ bib | Abstract ] |
| [19] | Existential Heap Abstraction Entailment is Undecidable. 10th Annual International Static Analysis Symposium. 2003. [ps] [ bib | Abstract ] |
| [18] | In-Place Refinement for Effect Checking. Workshop on Automated Verification of Infinite-State Systems. 2003. [ps] [ bib | Abstract ] |
| [17] | On the Theory of Structural Subtyping. MIT LCS Technical Report 879. 2003. [ps] [ bib | http | Abstract ] |
| [16] | Typestate Checking and Regular Graph Constraints. MIT LCS Technical Report 863. 2002. [ps] [ bib | http | Abstract ] |
| [15] | Role Analysis. ACM Symp. Principles of Programming Languages (POPL). 2002. [ps] [ bib | Abstract ] |
| [14] | Designing an Algorithm for Role Analysis. Master's Thesis, MIT LCS. 2001. [ps] [ bib | Abstract ] |
| [13] | Roles are really great!. MIT LCS Technical Report 822. 2001. [ps] [ bib | Abstract ] |
| [12] | A Language for Role Specifications. Workshop on Languages and Compilers for Parallel Computing. 2001. [ps] [ bib | Abstract ] |
| [11] | Object Models, Heaps, and Interpretations. MIT LCS Technical Report 816. 2001. [ps] [ bib | Abstract ] |
| [10] | Numerical Representations as Purely Functional Data Structures: A New Approach. INFORMATICA, Institute of Mathematics and Informatics, Vilnius. 2002. [ bib ] |
| [9] | Types and confluence in lambda calculus. 3rd Panhellenic Logic Symposium. 2001. [ bib ] |
| [8] | Confluence of untyped lambda calculus via simple types. Proceedings of the 7th Italian Conference on Theoretical Computer Science, ICTCS 2001. 2001. [ bib ] |
| [7] | Reducibility method for termination properties of typed lambda terms. Fifth International Workshop on Termination. 2001. [ bib ] |
| [6] | Modular Language Specifications in Haskell. Theoretical Aspects of Computer Science with practical application. 2000. [ps] [ bib | Abstract ] |
| [5] | Modular Interpreters in Haskell. B.Sc. Thesis, University of Novi Sad. 2000. [ps] [ bib ] |
| [4] | Numerical Representations as Purely Functional Data Structures. XIV Conference on Applied Mathematics PRIM, Palić. 2000. [ bib ] |
| [3] | Reducibility Method in Simply Typed Lambda Calculus. XIV Conference on Applied Mathematics PRIM, Palić. 2000. [ bib ] |
| [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] [ bib | Abstract ] |
| [1] | PLS: Programming Language for Simulations. Proceedings of the Petnica Science Center Seminar '93. 1993. [ bib | Abstract ] |