Viktor Kuncak
Associate Professor
viktor.kuncak@epfl.ch +41 21 693 52 81 http://lara.epfl.ch/~kuncak
Detailed page
https://lara.epfl.ch/~kuncak
EPFL IC IINFCOM LARA
INR 318 (Bâtiment INR)
Station 14
CH-1015 Lausanne
+41 21 693 52 81
+41 21 693 49 43
Office:
INR 318
EPFL
>
IC
>
IINFCOM
>
LARA
Web site: Web site: https://lara.epfl.ch
Fields of expertise
formal verification, theorem proving, program synthesis
Biography
Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 41. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification and at Coursera the MOOC "Parallel Programming".Education
PhD
MIT
2007
Publications
Infoscience publications
Infoscience
2023
Conference Papers
LISA – A Modern Proof System
2023-06-30. 14th Conference on Interactive Theorem Proving, Białystok, Poland, 2023, July 31 - August 4, 2023.Formula Normalizations in Verification
2023-06-16. 35th International Conference on Computer Aided Verification, Paris, France.The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
2023.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.Working Papers
The Complexity of Satisfiability Checking for Symbolic Finite Automata
2023-07-03Reports
On Algebraic Array Theories
20232022
Conference Papers
NP Satisfiability for Arrays as Powers
2022-01-14. 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.Generalized Arrays for Stainless Frames
2022-01-14. 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.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.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.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
2022-01-12Student Projects
Optimizing Java on Truffle
2022-05-10BPMN process generation and optimization for readability in the context of telemedecine
2022-04-232021
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
Journal Articles
Exploiting Errors for Efficiency: A Survey from Circuits to Applications
Acm Computing Surveys. 2020-06-01. DOI : 10.1145/3394898.Limits on amplifiers of natural selection under death-Birth updating
Plos Computational Biology. 2020-01-01. DOI : 10.1371/journal.pcbi.1007494.Conference Papers
Zippy LL(1) Parsing with Derivatives
2020-01-01. 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-12-01. DOI : 10.1007/s10703-017-0270-2.On the complexity of linearizability
Computing. 2019-09-01. DOI : 10.1007/s00607-018-0596-7.Population structure determines the tradeoff between fixation probability and fixation time
Communications Biology. 2019-04-23. DOI : 10.1038/s42003-019-0373-y.Theses
Verified Functional Programming
Lausanne, EPFL, 2019. DOI : 10.5075/epfl-thesis-9479.Scaling Functional Synthesis and Repair
Lausanne, EPFL, 2019. DOI : 10.5075/epfl-thesis-8716.2018
Conference Papers
Monotonic Prefix Consistency in Distributed Systems
2018-05-30. 38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Madrid, Spain, June 18-20, 2018. DOI : 10.1007/978-3-319-92612-4_3.2017
Journal Articles
Solving quantified linear arithmetic by counterexample-guided instantiation
Formal Methods in System Design. 2017-08-03. DOI : 10.1007/s10703-017-0290-y.Towards a Compiler for Reals
ACM Transactions on Programming Languages and Systems. 2017-05-01. DOI : 10.1145/3014426.Contract-Based Resource Verification for Higher-Order Functions with Memoization
Acm Sigplan Notices. 2017. DOI : 10.1145/3009837.3009874.Conference Papers
An Update on Deductive Synthesis and Repair in the Leon Tool
2017-05-03. p. 100-111. DOI : 10.4204/EPTCS.229.9.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.On verifying causal consistency
2017. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, January, 15-21, 2017. p. 626-638. DOI : 10.1145/3009837.3009888.Theses
Algorithmic Resource Verification
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7885.Interactive Programming by Example
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7956.Verification by Reduction to Functional Programs
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7636.Algorithmic Verification of Component-based Systems
Lausanne, EPFL, 2017. DOI : 10.5075/epfl-thesis-7753.Reports
Termination of Open Higher-Order Programs
2017Talks
Programmation Interactive par l'Exemple
Publish PhD Defense of Mikaël Mayer, EPFL, Lausanne, Switzerland, September 28, 2017.Student Projects
The Operational Semantics and Implementation of a Core Dart language
2017Extending Safe C Support In Leon
20172016
Conference Papers
Translating Scala Programs to Isabelle/HOL, Automated Reasoning
2016-06-12. p. 568-577. DOI : 10.1007/978-3-319-40229-1_38.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.A Scala Library for Testing Student Assignments on Concurrent Programming
2016. 7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016. p. 1-10. DOI : 10.1145/2998392.2998395.Theses
Deductive Synthesis and Repair
Lausanne, EPFL, 2016. DOI : 10.5075/epfl-thesis-6878.Reports
On Verifying Causal Consistency
2016Automating 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
Deductive Program Repair, Computer Aided Verification
2015-07-14. 27th International Conference on Computer-Aided Verification, San Francisco, CA, USA, July 18-24, 2015. p. 217-233. DOI : 10.1007/978-3-319-21668-3_13.Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Computer Aided Verification
2015-07-14. International Conference on Computer Aided Verification, San Francisco, July 18-24, 2015. p. 198-216. DOI : 10.1007/978-3-319-21668-3_12.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.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.A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
2015. 10th International Symposium on Frontiers of Combining Systems (FroCoS), Wroclaw, POLAND, SEP 21-24, 2015. p. 135-150. DOI : 10.1007/978-3-319-24246-0_9.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.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.A Decision Procedure for (Co)datatypes in SMT Solvers
2015. 25th International Conference on Automated Deduction (CADE), Berlin, GERMANY, AUG 01-07, 2015. p. 197-213. DOI : 10.1007/978-3-319-21401-6_13.Automating Grammar Comparison
2015. OOPSLA, Pittsburgh, PE, October 23-30, 2015. p. 183–200. DOI : 10.1145/2814270.2814304.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.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.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.Theses
Search Techniques for Code Generation
Lausanne, EPFL, 2015. DOI : 10.5075/epfl-thesis-6378.Reports
On Counter-Example Complete Verification for Higher-Order Functions
2015Towards Automating Grammar Equivalence Checking
2015On Deductive Program Repair in Leon
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.Modularity in the design of robust distributed algorithms
EPFL, 2014. DOI : 10.5075/epfl-thesis-6085.Reports
On Induction for SMT Solvers
2014On Synthesizing Code from Free-Form Queries
2014On Numerical Error Propagation with Sensitivity
2014Symbolic Resource Bound Inference
2014Student Projects
Contracts for Real-Time, Safety Critical Systems
20142013
Journal Articles
Functional synthesis for linear arithmetic and sets
International Journal on Software Tools for Technology Transfer. 2013. DOI : 10.1007/s10009-011-0217-7.Synthesis Modulo Recursive Functions
Acm Sigplan Notices. 2013. DOI : 10.1145/2509136.2509555.Software verification and graph similarity for automated evaluation of students' assignments
Information And Software Technology. 2013. DOI : 10.1016/j.infsof.2012.12.005.Conference Papers
Game Programming by Demonstration
2013. Onward! 2013, Indianapolis, Indiana, USA, October 2013. p. 75–90. DOI : 10.1145/2509578.2509583.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.An overview of the Leon verification system: verification by translation to recursive functions
2013. SCALA 2013, Montpellier, France, 2013. DOI : 10.1145/2489837.2489838.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.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.CafeSat: a Modern SAT Solver for Scala
2013. the 4th Scala Workshop, Montpellier, France, 02 07 2013. p. 1-4. DOI : 10.1145/2489837.2489839.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.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.Theses
Automatic Verification with Abstraction and Theorem Proving
Lausanne, EPFL, 2013. DOI : 10.5075/epfl-thesis-5828.Reports
On Repairing Ill-Typed Expressions
2013On Sound Compilation of Reals
2013On Verification by Translation to Recursive Functions
2013On Cafesat: A Modern SAT Solver for Scala
2013On Integrating Deductive Synthesis and Verification Systems
2013Techniques for Program Synthesis
2013On the Generation of Precise Fixed-Point Expressions
2013Student Projects
Interactive Code Generation
20132012
Journal Articles
Abortable Linearizable Modules
Archive of Formal Proofs. 2012.Speculative Linearizability
Acm Sigplan Notices. 2012. DOI : 10.1145/2254064.2254072.Symbolic execution of Reo circuits using constraint automata
Science Of Computer Programming. 2012. DOI : 10.1016/j.scico.2011.04.001.Constraints as Control
Acm Sigplan Notices (POPL). 2012. DOI : 10.1145/2103621.2103675.Software Synthesis Procedures
Communications of the ACM. 2012. DOI : 10.1145/2076450.2076472.Conference Papers
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.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.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.Theses
Programming with Specifications
Lausanne, EPFL, 2012. DOI : 10.5075/epfl-thesis-5581.Reports
On Complete Completion using Types and Weights
2012On Reductions for Synthesis Procedures
2012On 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 the Automatic Computation of Error Bounds for Solutions of Nonlinear Equations
2012On Accelerating Interpolants
2012On Synthesis for Unbounded Bit-vector Arithmetic
2012Talks
Leveraging Formal Verification Throughout the Entire Design Cycle
Design Verification Club Europe (DVClub 2012), November 21, 2012.Student Projects
Verification of Imperative Programs in Scala
20122011
Journal Articles
Measuring shape rectangularity
Electronics Letters. 2011. DOI : 10.1049/el.2011.0020.Formal Analysis of SystemC Designs in Process Algebra
Fundamenta Informaticae. 2011. DOI : 10.3233/FI-2011-391.Conference Papers
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.Decision Procedures for Automating Termination Proofs
2011. 12th International Conference on Verification, Model Checking, and Abstract Interpretation, Austin, TX, Jan 23-25, 2011. p. 371-386. DOI : 10.1007/978-3-642-18275-4_26.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.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.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.Interactive Synthesis of Code Snippets
2011. Computer Aided Verification (CAV), 2011.Scala to the Power of Z3: Integrating SMT and Programming
2011. Computer-Aideded Deduction (CADE).Satisfiability Modulo Recursive Programs
2011. Static Analysis Symposium (SAS), 2011. p. 298-315. DOI : 10.1007/978-3-642-23702-7_23.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
2011Code Completion using Quantitative Type Inhabitation
2011Speculative Linearizability
2011On an Efficient Decision Procedure for Imperative Tree Data Structures
2011On the Design and Implementation of SmartFloat and AffineFloat
2011On Interactive Synthesis of Code Snippets
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
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.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.Counterexample-Guided Focus
2010. 37th ACM-SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Madrid, SPAIN, Jan 17-23, 2010. p. 249-260. DOI : 10.1145/1706299.1706330.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.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.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.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.Automatic Verification of Parametric Specifications with Complex Topologies
2010. Integrated Formal Methods 2010, 8th International Conference, Nancy, France, October 11-14, 2010. p. 152–167. DOI : 10.1007/978-3-642-16265-7_12.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.Test Generation through Programming in UDITA
2010. International Conference on Software Engineering (ICSE), 2010. p. 225–234. DOI : 10.1145/1806799.1806835.Complete Functional Synthesis
2010. ACM Conference on Programming Language Design and Implementation (PLDI), 2010. p. 316–329. DOI : 10.1145/1806596.1806632.Reports
On Satisfiability Modulo Computable Functions
2010On Rigorous Numerical Computation as a Scala Library
2010On Complete Reasoning about Axiomatic Specifications
2010On Sets with Cardinality Constraints in Satisfiability Modulo Theories
2010On Deciding Functional Lists with Sublist Sets
2010On Locality of One-Variable Axioms and Piecewise Combinations
2010On Using Static Analysis to Detect Type Errors in PHP Applications
2010On Decision Procedures for Ordered Collections
2010Student Projects
Well-structured Petri Nets extensions with data
2010Complete Program Synthesis for Linear Arithmetic
2010Static Analysis for the PHP Language
20102009
Conference Papers
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.Simplifying Distributed System Development
2009. 12th Workshop on Hot Topics in Operating Systems.An Integrated Proof Language for Imperative Programs
2009. ACM Conf. Programming Language Design and Implementation (PLDI). p. 338–351. DOI : 10.1145/1542476.1542514.CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems
2009. 6th USENIX Symp. Networked Systems Design and Implementation (NSDI).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 Complete Functional Synthesis
2009On Test Generation through Programming in UDITA
2009On Decision Procedures for Collections, Cardinalities, and Relations
2009On Decision Procedures for Algebraic Data Types with Abstractions
2009On Combining Theories with Shared Set Operations
2009On Set-Driven Combination of Logics and Verifiers
2009Student Projects
Programming with Undo
2009Robust Dynamically Deployed Static Analysis for Java
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.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.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.Reports
On Delayed Choice Execution for Falsification
2008Constraint Solving for Software Reliability and Text Analysis
2008CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems
2008On Linear Arithmetic with Stars
2008On Static Analysis for Expressive Pattern Matching
2008Student Projects
Non-Clausal Satisfiability Modulo Theories
2008Decision Tree Learning for Drools
20082007
Conference Papers
Runtime Checking for Program Verification
2007. Runtime Verification, Vancover, Canada, March 13, 2007. p. 202-213. DOI : 10.1007/978-3-540-77395-5_17.Runtime Checking for Program Verification Systems
2007.Verifying Complex Properties using Symbolic Shape Analysis
2007.Polynomial Constraints for Sets with Cardinality Bounds
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.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.Theses
Modular Data Structure Verification
2007.Reports
Runtime Checking for Separation Logic
2007Decision Procedures for Multisets with Cardinality Constraints
2007Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-complete
20072006
Journal Articles
Deciding Boolean Algebra with Presburger Arithmetic
Journal of Automated Reasoning. 2006. DOI : 10.1007/s10817-006-9042-1.Modular Pluggable Analyses for Data Structure Consistency
IEEE Transactions on Software Engineering. 2006. DOI : 10.1109/TSE.2006.125.Conference Papers
Field Constraint Analysis
2006.An overview of the Jahob analysis system: Project Goals and Current Status
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
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.Decision Procedures for Set-Valued Fields
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.Relational Analysis of Algebraic Datatypes
2005. p. 207–216. DOI : 10.1145/1081706.1081740.Reports
On Field Constraint Analysis
2005On Algorithms and Complexity for Sets with Cardinality Constraints
2005On Relational Analysis of Algebraic Datatypes
20052004
Journal Articles
Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses
SIGPLAN Notices. 2004. DOI : 10.1145/981009.981016.Conference Papers
Combining Theorem proving with Static Analysis for Data Structure Consistency
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.Modular Pluggable Analyses for Data Structure Consistency
2004.Verifying a File System Implementation
2004.Reports
On Our Experience with Modular Pluggable Analyses
2004On Spatial Conjunction as Second-Order Logic
2004On Generalized Records and Spatial Conjunction in Role Logic
2004The First-Order Theory of Sets with Cardinality Constraints is Decidable
2004On Decision Procedures for Set-Valued Fields
2004On Verifying a File System Implementation
20042003
Conference Papers
Structural Subtyping of Non-Recursive Types is Decidable
2003. p. 96-107. DOI : 10.1109/LICS.2003.1210049.Existential Heap Abstraction Entailment is Undecidable
2003.In-Place Refinement for Effect Checking
2003.Reports
On Modular Pluggable Analyses Using Set Interfaces
2003On the Theory of Structural Subtyping
2003On Role Logic
2003On the Boolean Algebra of Shape Analysis Constraints
2003On computing the fixpoint of a set of boolean equations
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.Reducibility method for termination properties of typed lambda terms
2001.Types and confluence in lambda calculus
2001. p. 17-21.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.Modular Language Specifications in Haskell
2000.Reducibility Method in Simply Typed Lambda Calculus
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.Teaching & PhD
Teaching
Computer Science
Communication Systems
PhD Students
Bovel Matthieu Alexandre, Chassot Samuel, Gambhir Sankalp, Guilloud Simon, Milovancevic Dragana,Past EPFL PhD Students
Blanc Régis William , Darulova Eva , Edelmann Romain , Gvero Tihomir , Hojjat Hossein , Kandhadai Madhavan Ravichandhran , Kneuss Etienne , Koukoutos Emmanouil , Losa Giuliano , Mayer Mikaël , Piskac Ruzica , Raya Rodrigo , Schmid Georg Stefan , Suter Philippe Paul Henri , Voirol Nicolas Charles Yves , Wang Qiang ,Courses
Software construction
Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and
fundamental software construction concepts (reusability, abstraction, encapsulation, composition, proofs)
Computer language processing
We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into the new web standard for portable binaries called WebAssembly ( https://webassembly.org/ )
Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.