https://lara.epfl.ch/w/ 2026-07-07T00:11:16+0200 https://lara.epfl.ch/w/ https://lara.epfl.ch/w/lib/tpl/epflv2/images/favicon.ico text/html 2013-05-12T21:32:17+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/correspondoutput.txt?rev=1368387137&do=diff # No SinE strategy applied fof(c_0_1, axiom, (![X1]:?[X2]:r(X1,X2)) , file('example.p', axTotal)). fof(c_0_2, axiom, (![X1]:![X2]:(r(X1,X2)=>![X3]:r(X1,f(X2,X3)))) , file('example.p', axExtends)). fof(c_0_3, axiom, (![X1]:(p(X1)|p(f(X1,a)))) , file('example.p', axAlt)). fof(c_0_4, conjecture, (![X1]:?[X2]:(r(X1,X2)&p(X2))) , file('example.p', c)). fof(c_0_5, negated_conjecture, (~(![X1]:?[X2]:(r(X1,X2)&p(X2)))) ,inference(assume_negation, [status(cth)],[c_0_4])). fof(c_0_6, plain, (![X3]:?[X4]:r… text/html 2013-05-27T13:58:11+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/expressioncompiler.scala?rev=1369655891&do=diff Tiny Expression Compiler Proved Correct in Leon /* Expression compiler correctness. Viktor Kuncak and Filip Maric */ import leon.Utils._ import leon.Annotations._ object ExpressionCompiler { sealed abstract class Sign case class NUM(x : Int) extends Sign case object PLUS extends Sign sealed abstract class List case class Cons(head : Sign, tail : List) extends List case class Nil() extends List def single(x: Sign) = Cons(x, Nil()) sealed abstract class Expr case class … text/html 2013-04-24T16:30:31+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/labs_01?rev=1366813831&do=diff LAB 01 : Introduction to leon We will introduce you to the Leon online interface to verify programs. The Web interface is accessible at: http://lara.epfl.ch/leon/tutorials Leon Package A tentative self-contained release is available here: leon.tar.bz2. This packaged version has been tested for text/html 2013-02-27T16:52:31+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/labs_02?rev=1361980351&do=diff Lab 02 : An introduction to Leon's codebase In this lab, you will start working on the Leon codebase directly. You will have to implement a series of simple tasks that will introduce you to the important classes and structures of the Leon verification system. text/html 2013-03-15T03:16:10+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/labs_03?rev=1363313770&do=diff Labs 03 - Reasoning about execution times Setup You will have to pull this new phase (along with several other Leon-wide changes) from the sav2013-main repository. This will bootstrap your work. You need to update your repository according to our recent changes in order to prepare for this lab (follow the text/html 2013-02-27T16:59:06+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/labs_eclipse?rev=1361980746&do=diff Compiling Leon using Eclipse If you wish to use eclipse (against all our recommendations), we provide you with a project configuration that should help you get started. Downloading Eclipse You will need Eclipse 4.2 Juno: http://www.eclipse.org/downloads/packages/eclipse-ide-java-developers/junosr1 Installing the Scala IDE text/html 2013-03-12T15:14:58+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/labs_fetch?rev=1363097698&do=diff Fetching new files from our repository We will usually give you new stubs and files for each lab. Instead of sending you the files and letting you merge them within your repository, we will use the machinery provided by git to do this. We provide you with instructions on how to do that within Eclipse as well as in the command-line: text/html 2013-02-26T13:50:17+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/labs_setup?rev=1361883017&do=diff Labs Setup Step 1) Registration You need to register your group on the SAV 2013 web interface. Labs can be done alone or in pairs. We will not accept groups of more than 2 persons. Go the the following url to create your groups: http://larasrv05.epfl.ch/sav13 Once you create a group, we will create for you a git repository that contains files necessary for the labs. We recommend that you use a command-line interface to git. text/html 2013-04-09T21:18:40+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_01?rev=1365535120&do=diff Lecturecise 01: Introduction and Overview Slides: [pdf] Homework * Watch this lecture: <http://slideshot.epfl.ch/play/suri_moore> * Watch this lecture: * DOI link to paper: <http://dx.doi.org/10.1145/1925844.1926423> * (for the video, click the Source Materials tab, or here) * Obtain Calculus of computation textbook Some other nice material is available: text/html 2013-04-09T21:18:31+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_02?rev=1365535111&do=diff Lecturecise 2: Background Background review [Exercises] Propositional Logic Informally Propositional Logic Syntax Propositional Logic Semantics Normal Forms for Propositional Logic Predicate Logic Informally First-Order Logic Syntax First-Order Logic Semantics Normal Forms for First-Order Logic Semantic Argument Method Sets and Relations More on inductive invariants Code contracts Fun with Spec# [Solutions] [ Example of the pen-and-paper proof] for an invariant to be inductive. … text/html 2015-04-21T17:33:35+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_03?rev=1429630415&do=diff Lecturecise 03: Presburger Arithmetic and Quantifier Elimination [Slides] Further Notes and Examples of QE Applications of Quantifier Elimination Quantifier Elimination Definition QE from Conjunction of Literals Suffices Simple QE for Dense Linear Orders Simple QE for Integer Difference Inequalities Definition of Presburger Arithmetic QE for Presburger Arithmetic Here is also a [PDF] that does not have any folding/missing content issues. Exercise: eliminate quantifiers in the followi… text/html 2013-04-09T21:17:53+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_04?rev=1365535073&do=diff Lecturecise 04: From Programs to Formulas Slides: [pdf] Link from a past year: Compositional VCG text/html 2013-04-09T21:17:28+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_05?rev=1365535048&do=diff Lecturecise 5: Synthesis through Quantifier Elimination [Original Slides], [Slides with Scribbles] Click Here for Examples Leon system [Some Further Examples and Applications to Constraints on Sets] Further research papers and overviews: * Software Synthesis Procedures * Functional Synthesis for Linear Arithmetic and Sets * for the framework and algebraic data types, see: our VMCAI 2013 paper * overview [Slides about Complete Functional Synthesis] * longer tutorial slides: part … text/html 2013-03-11T17:03:41+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_06?rev=1363017821&do=diff Lecturecise 06: Modeling Loops and Recursion [Initial Slides], [annotated slides] Partial Order Lattice Fixpoint Theorems text/html 2013-03-14T09:47:34+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_07?rev=1363250854&do=diff Lecturecise 07: Computing Transitive Closure of Integer Relations [Slides] text/html 2013-04-09T21:16:52+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_08?rev=1365535012&do=diff Lecturecise 8: Recursion, Fixpoints, and Algebraic Data Type Ideas [Original Slides PDF] and [annotated pdf slides] text/html 2013-04-09T21:16:28+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_09?rev=1365534988&do=diff Lecturecise 9: Hoare Logic [ Slides PDF] [Solutions for exercises] text/html 2013-04-09T21:15:51+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_10?rev=1365534951&do=diff Lecturecise 10: Weakest Preconditions. Algebraic Data Types Slides (PDF): [original], [annotated] text/html 2013-04-14T10:24:33+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_11?rev=1365927873&do=diff Lecturecise 11: Type-Driven Synthesis Type-Driven Synthesis, presented by Tihomir Gvero. [Slides PDF] More information: [PLDI 2013 paper] text/html 2013-04-12T14:22:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_12?rev=1365769342&do=diff Lecturecise 12: Abstract Interpretation Ideas [Revised PDF Slides] [Solutions to exercises] text/html 2013-04-12T11:47:41+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_13?rev=1365760061&do=diff Lecturecise 13: Lattices [PDF slides] [Solutions to exercises] text/html 2013-04-24T13:38:11+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_14?rev=1366803491&do=diff Lecturecise 14: From Lattices to Abstract Interpretation [original PDF slides], [annotated slides] [Proofs of some lemmas] text/html 2013-04-17T11:38:48+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_15?rev=1366191528&do=diff Lecturecise 15 [Sharad Malik's slides] [Philippe's slides] More Material Propositional Logic Syntax Propositional Logic Semantics Substitution Theorems for Propositional Logic Normal Forms for Propositional Logic Proof Theory for Propositional Logic Definition of Propositional Resolution Deriving Propositional Resolution QBF and Quantifier Elimination DPLL Algorithm for SAT Advanced SAT solving Techniques References * Calculus of Computation Textbook, Chapter 1.7 text/html 2013-04-19T13:01:29+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_16?rev=1366369289&do=diff Lecturecise 16 [Annotated PDF] Two more examples: Sign Analysis and Constant Propagation Remember Products of Lattices Comparing Fixpoints of Sequences Intuition for Parallel and Iterative Updates Chaotic Iteration in Abstract Interpretation Widening in Variable Range Analysis text/html 2013-04-24T10:22:44+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_17?rev=1366791764&do=diff Lecturecise 17: Predicate Abstraction Abstract interpretation view: [annotated slides] Explanation of reachability trees: [reachability tree] Further reading [Slides on Predicate Abstraction] Abstract Interpretation with Conjunctions of Predicates Powerdomains for Finite Domains Powerset of Conjunctions of Predicates Precomputing Post in Predicate Abstraction Interpolation Analyses Based on Formulas References * [Blast Paper] * [Paper on Interpolation in Verification] * [ Abstr… text/html 2013-04-30T13:06:50+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_18?rev=1367320010&do=diff lecturecise 18 [revised slides] Interpolation text/html 2013-05-10T15:05:01+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_19?rev=1368191101&do=diff Lecturecise 19: Compactness For Propositional Logic. Normal Forms for First-Order Logic [Slides on Compactness] Semantics for First-Order Logic Normal Forms for First-Order Logic text/html 2015-04-21T17:33:35+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_20?rev=1429630415&do=diff Lecturecise 20: Herbrand's Theorem and Resolution for First-Order Logic [PDF Slides] Resolution Theorem Provers Example of a very good theorem prover: * E prover Our running example in latex: Input in TPTP3 format: fof(axTotal,axiom, ![X]:?[Y]: r(X,Y)). fof(axExtends,axiom, ![X]:![Y]: (r(X,Y) => ![Z]:r(X,f(Y,Z)))). fof(axAlt,axiom, ![X]: (p(X) | p(f(X,a)))). fof(c,conjecture, ![X]:?[Y]: (r(X,Y) & p(Y))). text/html 2013-05-19T20:54:42+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_21?rev=1368989682&do=diff Lecturecise 21: Some Decidable Logics of Sets and Relations Continuing Lecturecise 20 Finish example for ground and non-ground resolution: [pdf] Effectively Propositional Logic (EPR) and Importance of Finite Herbrand Universe * exists x1,...,xn. forall y1,...,ym. G text/html 2013-05-21T14:22:10+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_22?rev=1369138930&do=diff Monadic Second Order Logic [Slides] text/html 2013-05-24T03:36:14+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_23?rev=1369359374&do=diff SMT Solvers Part I First, from 10:15 to 10:50, we present the basic technology behind the SMT solvers. * [slides] * QF formula is satisfiable iff some disjunct is SAT * use SAT solver to cleverly enumerate disjuncts * suffices to solve conjunctions text/html 2013-05-30T04:52:42+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/lecturecise_24?rev=1369882362&do=diff Lecturecise 24: Modeling Arrays and Linked Structures ExpressionCompiler.scala * [core slides] * [further advanced topics] ([pptx]) * [Effect Analysis of Higher-Order Functions] text/html 2013-04-22T19:17:46+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/practice_quiz?rev=1366651066&do=diff Practice quiz This is the quiz we gave last year. Please note that the schedule and the order of the material we covered then was somewhat different. Please ask questions if anything is unclear. [Quiz PDF] [Solutions] text/html 2013-05-21T14:44:51+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/project_presentations?rev=1369140291&do=diff Project presentations Presentations will take place from 9:00am - 12:00pm in INR113. Note the different room and time. Each group will have 20min including questions. Schedule 9:00 Defining and Validating Business Specification Using Leon (Gorica) text/html 2015-03-02T14:53:04+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/project_suggestions?rev=1425304384&do=diff Project suggestions General info * You are, of course, free to suggest your own project and discuss it with us. * To ensure that everyone knows what they should do and we know what you are actually doing, you will submit a short (about 1-2 pages) proposal for the project you decide on. This should include e.g. deliverables in terms of code or algorithms, a plan of attack for your problem, more background references, examples, etc. Deadline is 10 April. text/html 2015-04-21T17:33:35+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/semantic_argument_method?rev=1429630415&do=diff Semantic Argument Method Suppose we want to prove the validity of a propositional logic formula . Several methods to do this exists, one of which is called the semantic argument method. We start the proof by assuming that a falsifying interpretation exists: text/html 2013-03-12T18:16:21+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/testtimes.scala?rev=1363108581&do=diff import leon.Utils._ /** * Code should be contained in a single top-level object */ object Test1 { /** * You can define Algebraic Data Types using abstract classes and case classes. */ abstract class List case class Cons(head: Int, tail: List) extends List case class Nil() extends List def size(l: List): Int = (l match { case Nil() => 0 case Cons(h, t) => 1+size(t) }) ensuring { _ >= 0 } def contains(l: List, v: Int): Boolean = (l match { case Nil() => fals… text/html 2013-06-01T22:55:18+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav13/top?rev=1370120118&do=diff Synthesis, Analysis, and Verification 2013 For Moodle page: click here The course will be similar to SAV 2012 and SAV 2011. (See there for overview as well.) We initially refresh our knowledge of logic and agree on notation, but for a more thorough introduction, in addition to many textbooks, you may wish to check the videos of