Viktor Kuncak
EPFL IC IINFCOM LARA
INR 318 (Bâtiment INR)
Station 14
1015 Lausanne
+41 21 693 52 81
+41 21 693 49 43
Office: INR 318
EPFL › IC › IINFCOM › LARA
Site web: https://lara.epfl.ch
+41 21 693 52 81
Office: INR 318
EPFL › IC › IC-SIN › SIN-ENS
Site web: https://sin.epfl.ch
+41 21 693 52 81
Office: INR 318
EPFL › IC › IC-SSC › SSC-ENS
Site web: https://ssc.epfl.ch
Prix et distinctions
European Research Council
2012
Publications représentatives
Deciding Boolean Algebra with Presburger Arithmetic
Viktor Kuncak, Hai Huu Nguyen, and Martin Rinard
Published in Journal of Automated Reasoning, 36(3), 2006 in
Modular Pluggable Analyses for Data Structure Consistency
Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard
Published in IEEE Transactions on Software Engineering, 32(12), 2006 in
Relational Analysis of Algebraic Datatypes
Viktor Kuncak and Daniel Jackson
Published in Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2005 in
Structural Subtyping of Non-Recursive Types is Decidable
Viktor Kuncak and Martin Rinard
Published in Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003 in
Role Analysis
Viktor Kuncak and Patrick Lam and Martin Rinard
Published in Proceedings of the 29th Annual ACM Symposium on Principles of Programming Languages, 2002 in
2025
Conference Papers
Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
2025. 26th International Conference on Verification, Model Checking, and Abstract Interpretation, Denver, CO, USA, 2025-01-20 - 2025-01-21. p. 185 - 207. DOI : 10.1007/978-3-031-82703-7_9.Formal Autograding in a Classroom
2025. European Symposium On Programming 2025.Theses
Automated Induction for Proving Program Equivalence
Lausanne, EPFL, 2025. DOI : 10.5075/epfl-thesis-10552.Working Papers
Interoperability of Proof Systems with SC-TPTP
20252024
Journal Articles
Succinct ordering and aggregation constraints in algebraic array theories
Journal Of Logical And Algebraic Methods In Programming. 2024. DOI : 10.1016/j.jlamp.2024.100978.Conference Papers
Verifying a Realistic Mutable Hash Table: Case Study (Short Paper)
2024. 12th International Joint Conference on Automated Reasoning, Nancy, France, 2024-07-03 - 2024-07-06. p. 304 - 314. DOI : 10.1007/978-3-031-63498-7_18.Interpolation and Quantifiers in Ortholattices
2024. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024), London, United Kingdom, January 15-16, 2024.Mechanized HOL Reasoning in Set Theory
2024. 15th International Conference on Interactive Theorem Proving (ITP 2024), Tbilisi, Georgia, September 9-14, 2024.Orthologic with Axioms
2024. 51st ACM SIGPLAN Symposium on Principles of Programming Languages, London, United Kingdom, 2024-01-17 - 2024-01-19. DOI : 10.1145/3632881.Interpolation and Quantifiers in Ortholattices
2024. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), London, ENGLAND, JAN 15-16, 2024. p. 235 - 257. DOI : 10.1007/978-3-031-50524-9_11.Working Papers
Proving Termination via Measure Transfer in Equivalence Checking
2024Reports
Proving Termination via Measure Transfer in Equivalence Checking (Extended Version)
20242023
Journal Articles
On algebraic array theories
Journal Of Logical And Algebraic Methods In Programming. 2023. DOI : 10.1016/j.jlamp.2023.100906.Conference Papers
LISA – A Modern Proof System
2023. 14th Conference on Interactive Theorem Proving, Białystok, Poland, 2023, July 31 - August 4, 2023. DOI : 10.4230/LIPIcs.ITP.2023.17.Formula Normalizations in Verification
2023. 35th International Conference on Computer Aided Verification, Paris, France.Proving and Disproving Equivalence of Functional Programming Assignments
2023. p. 928 - 951. DOI : 10.1145/3591258.Theses
Decision Procedures for Power Structures
Lausanne, EPFL, 2023. DOI : 10.5075/epfl-thesis-10546.Reports
On Algebraic Array Theories
20232022
Conference Papers
Generalized Arrays for Stainless Frames
2022. 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Philadelphia, PA, USA, January 16-18, 2022. p. 332 - 354. DOI : 10.1007/978-3-030-94583-1_17.NP Satisfiability for Arrays as Powers
2022. 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Philadelphia, PA, USA, January 16-18, 2022. DOI : 10.1007/978-3-030-94583-1_15.Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
2022. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2022), Munich, Germany, April 2-7, 2022. p. 196 - 214. DOI : 10.1007/978-3-030-99527-0_11.From Verified Scala to STIX File System Embedded Code Using Stainless
2022. 14th International Symposium NASA Formal Methods (NFM 2022), Pasadena, CA, USA, May 24–27, 2022. p. 393 - 410. DOI : 10.1007/978-3-031-06773-0_21.Formally Verified Quite OK Image Format
2022. Formal Methods in Computer-Aided Design 2022, Trento, Italy, October 17-21, 2022. p. 343 - 348. DOI : 10.34727/2022/isbn.978-3-85448-053-2_41.Theses
Scaling Language Features for Program Verification
Lausanne, EPFL, 2022. DOI : 10.5075/epfl-thesis-8030.Reports
On Verified Scala for STIX File System Embedded Code using Stainless
2022Student Projects
Optimizing Java on Truffle
2022BPMN process generation and optimization for readability in the context of telemedecine
20222021
Theses
Efficient Parsing with Derivatives and Zippers
Lausanne, EPFL, 2021. DOI : 10.5075/epfl-thesis-7357.Student Projects
Formal Verification of Rust with Stainless
20212020
Conference Papers
Zippy LL(1) Parsing with Derivatives
2020. 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ELECTR NETWORK, Jun 15-20, 2020. p. 1036 - 1051. DOI : 10.1145/3385412.3385992.2019
Journal Articles
Refutation-based synthesis in SMT
Formal Methods In System Design. 2019. DOI : 10.1007/s10703-017-0270-2.Theses
Scaling Functional Synthesis and Repair
Lausanne, EPFL, 2019. DOI : 10.5075/epfl-thesis-8716.Verified Functional Programming
Lausanne, EPFL, 2019. DOI : 10.5075/epfl-thesis-9479.2017
Journal Articles
Solving quantified linear arithmetic by counterexample-guided instantiation
Formal Methods in System Design. 2017. DOI : 10.1007/s10703-017-0290-y.Contract-Based Resource Verification for Higher-Order Functions with Memoization
Acm Sigplan Notices. 2017. DOI : 10.1145/3009837.3009874.Conference Papers
Proactive Synthesis of Recursive Tree-to-String Functions from Examples
2017. European Conference on Object-Oriented Programming, Barcelona, Spain, Sun 18 - Fri 23 June 2017.Theses
Verification by Reduction to Functional Programs
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7636.Interactive Programming by Example
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7956.Algorithmic Verification of Component-based Systems
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7753.Algorithmic Resource Verification
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7885.Reports
Termination of Open Higher-Order Programs
2017Student Projects
Extending Safe C Support In Leon
2017The Operational Semantics and Implementation of a Core Dart language
20172016
Conference Papers
SMT-Based Checking of Predicate-Qualified Types for Scala
2016. 7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016. p. 31 - 40. DOI : 10.1145/2998392.2998398.Theses
Deductive Synthesis and Repair
Lausanne, EPFL, 2016. DOI : 10.5075/epfl-thesis-6878.Reports
Automating Verification of Functional Programs with Quantified Invariants
2016Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization
2016On Satisfiability for Quantified Formulas in Instantiation-Based Procedures
20162015
Journal Articles
On recursion-free Horn clauses and Craig interpolation
Formal Methods In System Design. 2015. DOI : 10.1007/s10703-014-0219-7.Conference Papers
Developing Verified Software Using Leon
2015. 7th NASA Formal Methods Symposium (NFM), Pasadena, CA, APR 27-29, 2015. p. 12 - 15. DOI : 10.1007/978-3-319-17524-9_2.Sound reasoning about integral data types with a reusable SMT solver interface
2015. the 6th ACM SIGPLAN Symposium, Portland, OR, USA, 13 06 2015. p. 35 - 40. DOI : 10.1145/2774975.2774980.Synthesizing Functions from Relations in Leon
2015. 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Univ Kent, Canterbury, ENGLAND, SEP 09-11, 2014.Automating Grammar Comparison
2015. OOPSLA, Pittsburgh, PE, October 23-30, 2015. p. 183 - 200. DOI : 10.1145/2814270.2814304.Synthesizing Java Expressions from Free-Form Queries
2015. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015. p. 416 - 432. DOI : 10.1145/2814270.2814295.Induction for SMT Solvers
2015. 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Mumbai, INDIA, JAN 12-14, 2015. p. 80 - 98. DOI : 10.1007/978-3-662-46081-8_5.Programming with Enumerable Sets of Structures
2015. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, OCT 25-30, 2015. p. 37 - 56. DOI : 10.1145/2814270.2814323.Interactive Synthesis using Free-Form Queries
2015. International Conference on Software Engineering, Demo Papers (ICSE Demo 2015), Florence, Italy, May 16-24, 2015. p. 689 - 692. DOI : 10.1109/ICSE.2015.224.Theses
Search Techniques for Code Generation
Lausanne, EPFL, 2015. DOI : 10.5075/epfl-thesis-6378.Reports
Towards Automating Grammar Equivalence Checking
2015On Deductive Program Repair in Leon
2015On Counter-Example Complete Verification for Higher-Order Functions
20152014
Conference Papers
Verifying and Synthesizing Software with Recursive Functions
2014. 41st International Colloquium on Automata, Languages and Programming. p. 11 - 25. DOI : 10.1007/978-3-662-43948-7_2.Sound Compilation of Reals
2014. 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)', u'41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). p. 235 - 248. DOI : 10.1145/2535838.2535874.Theses
Programming with Numerical Uncertainties
Lausanne, EPFL, 2014. DOI : 10.5075/epfl-thesis-6343.Reports
On Induction for SMT Solvers
2014Symbolic Resource Bound Inference
2014On Synthesizing Code from Free-Form Queries
2014On Numerical Error Propagation with Sensitivity
2014Student Projects
Contracts for Real-Time, Safety Critical Systems
20142013
Journal Articles
Software verification and graph similarity for automated evaluation of students' assignments
Information And Software Technology. 2013. DOI : 10.1016/j.infsof.2012.12.005.Functional synthesis for linear arithmetic and sets
International Journal on Software Tools for Technology Transfer. 2013. DOI : 10.1007/s10009-011-0217-7.Conference Papers
An overview of the Leon verification system: verification by translation to recursive functions
2013. SCALA 2013, Montpellier, France, 2013. DOI : 10.1145/2489837.2489838.Automatic Synthesis of Out-of-Core Algorithms
2013. ACM SIGMOD International Conference on Management of Data, New York, NY, USA, June 22-27, 20013. p. 133 - 144. DOI : 10.1145/2463676.2465334.Interpolation for Synthesis on Unbounded Domains
2013. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, OCT 20-23, 2013. p. 93 - 96. DOI : 10.1109/FMCAD.2013.6679396.Synthesis of Fixed-Point Programs
2013. International Conference on Embedded Software (EMSOFT), Montreal, Canada, Sept 29 - Oct 04, 2013. DOI : 10.1109/EMSOFT.2013.6658600.Effect Analysis for Programs with Callbacks
2013. Verified Software: Theories, Tools, Experiments, Menlo Park, CA, USA, 2013. p. 48 - 67. DOI : 10.1007/978-3-642-54108-7_3.Complete Completion using Types and Weights
2013. 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). p. 27 - 38. DOI : 10.1145/2491956.2462192.Certifying Solutions for Numerical Constraints
2013. Third International Conference on Runtime Verification, Istanbul, Turkey, September 25-28, 2012. p. 277 - 291. DOI : 10.1007/978-3-642-35632-2_27.Game Programming by Demonstration
2013. Onward! 2013, Indianapolis, Indiana, USA, October 2013. p. 75 - 90. DOI : 10.1145/2509578.2509583.Theses
Automatic Verification with Abstraction and Theorem Proving
Lausanne, EPFL, 2013. DOI : 10.5075/epfl-thesis-5828.Reports
On the Generation of Precise Fixed-Point Expressions
2013On Verification by Translation to Recursive Functions
2013On Integrating Deductive Synthesis and Verification Systems
2013On Sound Compilation of Reals
2013Student Projects
Termination Analysis in a Higher-Order Functional Context
2013Interactive Code Generation
20132012
Journal Articles
Abortable Linearizable Modules
Archive of Formal Proofs. 2012.Software Synthesis Procedures
Communications of the ACM. 2012. DOI : 10.1145/2076450.2076472.Speculative Linearizability
Acm Sigplan Notices. 2012. DOI : 10.1145/2254064.2254072.Constraints as Control
Acm Sigplan Notices (POPL). 2012. DOI : 10.1145/2103621.2103675.Conference Papers
Constraints as Control
2012. 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, Jan 25-27, 2012. p. 151 - 164. DOI : 10.1145/2103656.2103675.Accelerating Interpolants
2012. 10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, India, October 3-6, 2012. p. 187 - 202. DOI : 10.1007/978-3-642-33386-6_16.A Verification Toolkit for Numerical Transition Systems
2012. 18th International Symposium on Formal Methods, Paris, France, August 27-31, 2012. p. 247 - 251. DOI : 10.1007/978-3-642-32759-9_21.Theses
Programming with Specifications
Lausanne, EPFL, 2012. DOI : 10.5075/epfl-thesis-5581.Reports
On Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments
2012On Fast Code Completion using Type Inhabitation
2012On Effect Analysis for Programs with Callbacks
2012On Reductions for Synthesis Procedures
2012On Complete Completion using Types and Weights
2012On Accelerating Interpolants
2012On Synthesis for Unbounded Bit-vector Arithmetic
2012On the Automatic Computation of Error Bounds for Solutions of Nonlinear Equations
2012Student Projects
Verification of Imperative Programs in Scala
20122011
Conference Papers
Interactive Synthesis of Code Snippets
2011. Computer Aided Verification (CAV), 2011.Scala to the Power of Z3: Integrating SMT and Programming
2011. 23rd International Conference on Automated Deduction (CADE 23). p. 400 - 406. DOI : 10.1007/978-3-642-22438-6_30.Satisfiability Modulo Recursive Programs
2011. Static Analysis Symposium (SAS), 2011. p. 298 - 315. DOI : 10.1007/978-3-642-23702-7_23.Towards Complete Reasoning about Axiomatic Specifications
2011. Verification, Model Checking, and Abstract Interpretation (VMCAI). p. 278 - 293. DOI : 10.1007/978-3-642-18275-4_20.Scala to the Power of Z3: Integrating SMT and Programming
2011. Computer-Aideded Deduction (CADE).Sets with Cardinality Constraints in Satisfiability Modulo Theories
2011. Verification, Model Checking, and Abstract Interpretation (VMCAI). p. 403 - 418. DOI : 10.1007/978-3-642-18275-4_28.Trustworthy Numerical Computation in Scala
2011. ACM Conf. on Object-Oriented Programming, Systems, Languages, and Applications, Portland, Oregon, USA, October 25-27. p. 325 - 344. DOI : 10.1145/2076021.2048094.Theses
Decision Procedures for Program Synthesis and Verification
Lausanne, EPFL, 2011. DOI : 10.5075/epfl-thesis-5220.Reports
PhoneLab: Cloud-Backed Development Environment for Smartphones
2011On an Efficient Decision Procedure for Imperative Tree Data Structures
2011Code Completion using Quantitative Type Inhabitation
2011On the Design and Implementation of SmartFloat and AffineFloat
2011On Interactive Synthesis of Code Snippets
2011Speculative Linearizability
2011Student Projects
Toward Interprocedural Pointer and Effect Analysis for Scala
20112010
Journal Articles
Predicting and Preventing Inconsistencies in Deployed Distributed Systems
ACM Transactions on Computer Systems. 2010. DOI : 10.1145/1731060.1731062.Conference Papers
Complete Functional Synthesis
2010. ACM Conference on Programming Language Design and Implementation (PLDI), 2010. p. 316 - 329. DOI : 10.1145/1806596.1806632.Comfusy: A Tool for Complete Functional Synthesis
2010. 22nd International Conference on Computer Aided Verification, Edinburgh, Scotland, UK, July 15-19, 2010. p. 430 - 433. DOI : 10.1007/978-3-642-14295-6_38.Test Generation through Programming in UDITA
2010. International Conference on Software Engineering (ICSE), 2010. p. 225 - 234. DOI : 10.1145/1806799.1806835.Ordered Sets in the Calculus of Data Structures
2010. 19th Annual Conference of the European Association for Computer Science Logic, Brno, Czech Republic, August 23-27, 2010. p. 34 - 48. DOI : 10.1007/978-3-642-15205-4_5.Runtime Instrumentation for Precise Flow-Sensitive Type Analysis
2010. Runtime Veritication, St. Julians, Malta, November 1-4, 2010. p. 300 - 314. DOI : 10.1007/978-3-642-16612-9_23.MUNCH - Automated Reasoner for Sets and Multisets
2010. International Joint Conference on Automated Reasoning, Edinburgh, UK, July 16-19, 2010. p. 149 - 155. DOI : 10.1007/978-3-642-14203-1_13.Phantm: PHP analyzer for type mismatch
2010. FSE '10 Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering, Santa-Fe, NM, USA, November 7-11 2010. p. 373 - 374. DOI : 10.1145/1882291.1882355.Building a Calculus of Data Structures
2010. 11th International Conference on Verification, Model Checking and Abstract Interpretation, Madrid, Spain, January 17-19, 2010. p. 26 - 44. DOI : 10.1007/978-3-642-11319-2_6.Collections, Cardinalities, and Relations
2010. p. 380 - 395. DOI : 10.1007/978-3-642-11319-2_27.Decision Procedures for Algebraic Data Types with Abstractions
2010. ACM Symp. Principles of Programming Languages (POPL), 2010. p. 199 - 210. DOI : 10.1145/1706299.1706325.Reports
On Sets with Cardinality Constraints in Satisfiability Modulo Theories
2010On Locality of One-Variable Axioms and Piecewise Combinations
2010On Rigorous Numerical Computation as a Scala Library
2010On Complete Reasoning about Axiomatic Specifications
2010On Using Static Analysis to Detect Type Errors in PHP Applications
2010On Deciding Functional Lists with Sublist Sets
2010On Satisfiability Modulo Computable Functions
2010On Decision Procedures for Ordered Collections
2010Student Projects
Complete Program Synthesis for Linear Arithmetic
2010Static Analysis for the PHP Language
20102009
Conference Papers
CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems
2009. 6th USENIX Symp. Networked Systems Design and Implementation (NSDI).An Integrated Proof Language for Imperative Programs
2009. ACM Conf. Programming Language Design and Implementation (PLDI). p. 338 - 351. DOI : 10.1145/1542476.1542514.Simplifying Distributed System Development
2009. 12th Workshop on Hot Topics in Operating Systems.Combining Theories with Shared Set Operations
2009. 7th International Symposium on Frontiers of Combining Systems, Trento, Italy, September 16-18, 2009. p. 366 - 382. DOI : 10.1007/978-3-642-04222-5_23.Opis: Reliable Distributed Systems in OCaml
2009. ACM SIGPLAN Workshop on Types in Language Design and Implementation. p. 65 - 78. DOI : 10.1145/1481861.1481870.Reports
On Decision Procedures for Collections, Cardinalities, and Relations
2009On Set-Driven Combination of Logics and Verifiers
2009On Complete Functional Synthesis
2009On Test Generation through Programming in UDITA
2009On Combining Theories with Shared Set Operations
2009On Decision Procedures for Algebraic Data Types with Abstractions
2009Student Projects
Robust Dynamically Deployed Static Analysis for Java
2009Programming with Undo
2009State Exploration of Scala Actor Programs
20092008
Conference Papers
Runtime Checking for Separation Logic
2008. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), San Francisco, USA, January 7-9, 2008. p. 203 - 217. DOI : 10.1007/978-3-540-78163-9_19.Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars
2008. Computer Science Logic (CSL), 2008. p. 124 - 138. DOI : 10.1007/978-3-540-87531-4_11.Decision Procedures for Multisets with Cardinality Constraints
2008. 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), San Francisco, January 2008. p. 218 - 232. DOI : 10.1007/978-3-540-78163-9_20.Linear Arithmetic with Stars
2008. 20th International Conference on Computed-Aided Verification (CAV), Princeton, NJ, USA, July 7-14, 2008. p. 268 - 280. DOI : 10.1007/978-3-540-70545-1_25.Full Functional Verification of Linked Data Structures
2008. ACM Conf. Programming Language Design and Implementation (PLDI). p. 349 - 361. DOI : 10.1145/1375581.1375624.Reports
CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems
2008On Delayed Choice Execution for Falsification
2008On Static Analysis for Expressive Pattern Matching
2008Constraint Solving for Software Reliability and Text Analysis
2008On Linear Arithmetic with Stars
2008Student Projects
Non-Clausal Satisfiability Modulo Theories
2008Decision Tree Learning for Drools
20082007
Conference Papers
Polynomial Constraints for Sets with Cardinality Bounds
2007.Runtime Checking for Program Verification Systems
2007.Using First-Order Theorem Provers in the Jahob Data Structure Verification System
2007. p. 74 - 88. DOI : 10.1007/978-3-540-69738-1_5.Verifying Complex Properties using Symbolic Shape Analysis
2007.Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
2007. Conference on Automateded Deduction (CADE-21). p. 215 - 230. DOI : 10.1007/978-3-540-73595-3_15.Theses
Modular Data Structure Verification
2007.Reports
Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete
2007Decision Procedures for Multisets with Cardinality Constraints
2007Runtime Checking for Separation Logic
20072006
Journal Articles
Modular Pluggable Analyses for Data Structure Consistency
IEEE Transactions on Software Engineering. 2006. DOI : 10.1109/TSE.2006.125.Deciding Boolean Algebra with Presburger Arithmetic
Journal of Automated Reasoning. 2006. DOI : 10.1007/s10817-006-9042-1.Conference Papers
An overview of the Jahob analysis system: Project Goals and Current Status
2006.Field Constraint Analysis
2006.Reports
On Verifying Complex Properties using Symbolic Shape Analysis
2006On Using First-Order Theorem Provers in a the Jahob Data Structure Verification System
20062005
Conference Papers
Relational Analysis of Algebraic Datatypes
2005. p. 207 - 216. DOI : 10.1145/1081706.1081740.Hob: A Tool for Verifying Data Structure Consistency
2005.Generalized Typestate Checking for Data Structure Consistency
2005. p. 430 - 447. DOI : 10.1007/978-3-540-30579-8_28.Cross-Cutting Techniques in Program Specification and Analysis
2005.An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
2005. 20th International Conference on Automated Deduction, CADE-20. p. 260 - 277. DOI : 10.1007/11532231_20.Implications of a Data Structure Consistency Checking System
2005.Decision Procedures for Set-Valued Fields
2005.Reports
On Relational Analysis of Algebraic Datatypes
2005On Algorithms and Complexity for Sets with Cardinality Constraints
2005On Field Constraint Analysis
20052004
Journal Articles
Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses
SIGPLAN Notices. 2004. DOI : 10.1145/981009.981016.Conference Papers
Modular Pluggable Analyses for Data Structure Consistency
2004.Combining Theorem proving with Static Analysis for Data Structure Consistency
2004.Verifying a File System Implementation
2004.Generalized Records and Spatial Conjunction in Role Logic
2004.Boolean Algebra of Shape Analysis Constraints
2004. p. 59 - 72. DOI : 10.1007/978-3-540-24622-0_7.Reports
On Decision Procedures for Set-Valued Fields
2004The First-Order Theory of Sets with Cardinality Constraints is Decidable
2004On Spatial Conjunction as Second-Order Logic
2004On Our Experience with Modular Pluggable Analyses
2004On Verifying a File System Implementation
2004On Generalized Records and Spatial Conjunction in Role Logic
20042003
Conference Papers
Existential Heap Abstraction Entailment is Undecidable
2003.In-Place Refinement for Effect Checking
2003.Structural Subtyping of Non-Recursive Types is Decidable
2003. p. 96 - 107. DOI : 10.1109/LICS.2003.1210049.Reports
On Role Logic
2003On the Theory of Structural Subtyping
2003On the Boolean Algebra of Shape Analysis Constraints
2003On computing the fixpoint of a set of boolean equations
2003On Modular Pluggable Analyses Using Set Interfaces
20032002
Journal Articles
Numerical Representations as Purely Functional Data Structures: A New Approach
INFORMATICA, Institute of Mathematics and Informatics, Vilnius. 2002.Conference Papers
Role Analysis
2002. p. 17 - 32. DOI : 10.1145/503272.503276.Reports
Typestate Checking and Regular Graph Constraints
20022001
Conference Papers
A Language for Role Specifications
2001. 14th International Workshop on Languages and Compilers for Parallel Computing LCPC 2001, Cumberland Falls, KY, USA, August 1–3, 2001. p. 366 - 382. DOI : 10.1007/3-540-35767-X_24.Types and confluence in lambda calculus
2001. p. 17 - 21.Reducibility method for termination properties of typed lambda terms
2001.Confluence of untyped lambda calculus via simple types
2001. 7th Italian Conference on Theoretical Computer Science, ICTCS 2001, Torino, Italy, October 4–6, 2001. p. 38 - 49. DOI : 10.1007/3-540-45446-2_3.Reports
Object Models, Heaps, and Interpretations
2001Roles are really great!
2001Student Projects
Designing an Algorithm for Role Analysis
20012000
Conference Papers
Numerical Representations as Purely Functional Data Structures
2000.Reducibility Method in Simply Typed Lambda Calculus
2000.Modular Language Specifications in Haskell
2000.Student Projects
Modular Interpreters in Haskell
20001996
Student Projects
Developing a Multigrid Solver for Standing Wave Equation
19961993
Conference Papers
PLS: Programming Language for Simulations
1993. p. 111 - 146.Enseignement et PhD
Doctorant·es actuel·les
Matthieu Bovel, Auguste Poiroux, Sankalp Gambhir, Samuel Chassot, Simon Guilloud, Lazar Milikic
A dirigé les thèses EPFL de
Ruzica Piskac, Philippe Suter, Hossein Hojjat, Eva Darulova, Tihomir Gvero, Etienne Kneuss, Régis William Blanc, Mikaël Mayer, Qiang Wang, Ravichandhran Kandhadai Madhavan, Nicolas Voirol, Manos Koukoutos, Romain Edelmann, Georg Stefan Schmid, Rodrigo Raya, Dragana Milovancevic
A co-dirigé les thèses EPFL de
Cours
Computer language processing
CS-320
Nous enseignons les aspects fondamentaux de l'analyse et l'interprétation des langages informatiques, y compris les techniques pour construire des compilateurs. Le nouveau titre est "Traitement des langages informatiques".
Formal verification
CS-550
Software construction
CS-214
Apprenez à concevoir et à implémenter des logiciels fiables, maintenables et efficaces à l'aide de techniques variées (style déclaratif, fonctions d'ordre supérieur, types inductifs, parallélisme) et de concepts fondamentaux (réutilisabilité, abstraction, encapsulation, composition, preuves)