https://lara.epfl.ch/w/ 2026-06-23T17:02:28+0200 https://lara.epfl.ch/w/ https://lara.epfl.ch/w/lib/tpl/epflv2/images/favicon.ico text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/abstract_interpretation_of_transition_system?rev=1429630462&do=diff Abstract Interpretation of a Transition System Computing Invariants in a Transition System Transition system is given by a set of initial states, and one relation . * relation specifies one step of a system * we have seen that we can derive such relation from control-flow graph text/html 2010-05-10T12:16:04+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/application_of_exists-forall_decidability?rev=1273486564&do=diff Deciding a Language of Sets (and Relations) Language Consider a simple language of sets, motivated by verification of programs that manipulate containers: [Set-Valued Fields Motivation] [Set-Valued Fields Logic] Question: how do we justify ? Idea of Decidability We show that this language is decidable by reduction to universal class. text/html 2010-05-28T01:54:21+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/circularlist.java?rev=1275004461&do=diff class Node { public /*: claimedby CircularList */ Node next; public /*: claimedby CircularList */ Node prev; } class CircularList { private static Node first; private static Node last; /*: private static ghost specvar next1 :: "obj => obj" = "(\<lambda> x. null)"; public static specvar content :: objset; vardefs "content == {x. x ~= null & (first,x) : {(v,w). v..next1=w}^*}"; private static specvar isLast :: "obj => bool"; vardefs "isLast == (\<l… text/html 2010-12-01T18:03:15+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/course_information?rev=1291222995&do=diff Course Information: Synthesis, Analysis, and Verification 2010 Teaching Staff This class is taught in Spring 2010. The overall content is similar to past courses: * SAV 2009 * SAV 2008 Teaching staff: * Viktor Kuncak (lecturer) * Ruzica Piskac (PhD assistant) * Hossein Hojjat (PhD assistant) text/html 2010-05-28T01:49:37+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/cursorlist.java?rev=1275004177&do=diff class Node { public Object data; public /*: claimedby CursorList */ Node next; } class CursorList { private Node first; private Node iterPos; private Node iterPrev; /*: invariant prevDef: "iterPos ~= first --> iterPrev : content & iterPrev..next = iterPos"; invariant prevElse: "iterPos = first --> iterPrev = null"; public specvar currentIter :: obj; vardefs "currentIter == iterPos"; public ensured invariant iterInv: "(iter = {} -->… text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/deciding_exists-forall_class?rev=1429630462&do=diff Deciding Exists-Forall Class Theorem: Consider formula of the form where is quantifier free formula of first-order logic with equality, without function symbols (only constants and relation symbols). Then there exists a structure in which the formula is true iff the formula is true in some structure whose domain is the set of constants in text/html 2010-05-31T14:26:18+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/example_with_procedures?rev=1275308778&do=diff Example with Procedures proc main() { while (...) { p1(); p2(); } } proc p1() { open(); readContent(); } proc p2() { startLog(); readContent(); stopLog(); close(); } proc readContent() { while (...) { if (...) { read(); } else { print(); } } } text/html 2010-03-04T12:03:08+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/exercises_01?rev=1267700588&do=diff Exercises 01 For next time, please try to bring a laptop with installed: * PiVC * Isabelle, with working Nitpick Background Propositional Logic Informally Propositional Logic Syntax * Scala syntax trees Propositional Logic Semantics * Scala functions from booleans to booleans. Formula evaluator Normal Forms for Propositional Logic Proof Theory for Propositional Logic SAT Solvers DPLL Algorithm for SAT Advanced SAT solving Techniques Simple SAT Solver Simple Encodings into … text/html 2010-03-01T13:52:24+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/exercises_02?rev=1267447944&do=diff Sets and Relations Sets and Relations - useful preparation for program semantics First-Order Logic First-Order Logic, also called predicate logic or predicate calculus, extends propositional Logic with functions, relations, and quantification over individuals. Topics text/html 2010-03-30T16:05:19+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/exercises_06?rev=1269957919&do=diff Recall the definitions of Partial Order and Lattices. * Prove the following: * Examples of Lattices * Products of Lattices text/html 2010-04-23T09:58:26+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/exercises_09?rev=1272009506&do=diff Exercises 09 Applications of quantifier elimination List of Theories Admitting QE Simple QE for Dense Linear Orders Simple QE for Integer Difference Inequalities QE for Presburger Arithmetic Small Solutions for Quantifier-Free Presburger Arithmetic Deciding Boolean Algebra with Presburger Arithmetic text/html 2010-04-28T20:39:57+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/exercises_10?rev=1272479997&do=diff Exercises 10 Solutions of Homework 02 and Homework 03 Invariants Space [slides by Zohar Manna on quantifier elimination] About Quiz The quiz covers the material from Lecture 04 until the last lecture, including e.g. symbolic execution, abstract interpretation, and quantifier elimination. It is understood that you also know how to use sets, relations, and first-order logic, where needed. text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/homework_01?rev=1429630462&do=diff Homework 01: Due March 2, at 16:00 Problem 0: Simple preparatory steps * If you think you may attend the class, send emails to {viktor.kuncak, ruzica.piskac, hossein.hojjat} saying that you plan to attend. Also, please register in the online system. text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/homework_02?rev=1429630462&do=diff Homework 02: Due April 3rd at 10:00 on Moodle Upload your solution in PDF format to Moodle. Recall the definition of loop invariants. For the following two problems first find a reasonable precondition and postcondition for the function (in particular, precondition should be as weak as possible to enable correct execution, and postcondition should describe the result as accurately as possible). Then come up with loop invariants that prove that these programs correct. text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/homework_03?rev=1429630462&do=diff Homework 03: Due April 16 Problem 1 Let be the set of all first-order formulas (viewed as syntax trees, so e.g. is a different formula from ) and let be the implication relation on formulas: Check whether is reflexive, antisymmetric, and transitive relation. text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/homework_03_solutions?rev=1429630462&do=diff Homework 03: Solutions Problem 1 Let be the set of all first-order formulas (viewed as syntax trees, so e.g. is a different formula from and let be the implication relation on formulas: Check whether is reflexive, antisymmetric, and transitive relation. text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/invariants_exercises?rev=1429630462&do=diff Space of Invariants Problem Statement Let be a set (e.g. the set of all integers). Let and . Define For each element we have and we think of as an invariant. Prove each of the following statements or give a counterexample. a): If , then . text/html 2010-03-29T12:38:07+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/labs_05?rev=1269859087&do=diff Labs 05 Homework 02 discussion Project ideas * presentation of Etienne Kneuss * presentation of Stefan Bucur on projects from DSLab text/html 2011-02-15T20:34:04+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_01?rev=1297798444&do=diff Lecture 01: Introduction to Verification and Background Verification as Science - Basic Methodology Proving Correctness of Some Small Examples - Demos Importance of Verification - Uses of Verification Background Propositional Logic Informally - Propositional Logic is the core logical reasoning Predicate Logic Informally - We build on propositional logic to explain first-order predicate logic. text/html 2010-03-02T18:46:44+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_02?rev=1267552004&do=diff Lecture 02: From Programs to Relations Background: Sets and relations and [book chapter] Big Picture of VCG - Approach to Verification. Simple Programming Language - Turing-complete imperative language which we will use to illustrate verification. Relational Semantics - Specifying meaning of programs using relations, their composition, union and transitive closure. text/html 2010-03-09T15:07:42+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_03?rev=1268143662&do=diff Lecture 03: Hoare Logic and Formulas Remember Relational Semantics Hoare Logic Basics - Hoare Triple, Strongest Postcondition, Weakest Precondition, Non-deterministic loops Formulas Formulas and Relations - Moving from abstract relation representations towards formulas that describe relations Compositional VCG - Computing Formulas for Loop-Free Commands by Following Program Structure text/html 2010-03-09T17:11:39+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_03a?rev=1268151099&do=diff Lecture 03a: From Programs to Formulas Compositional VCG - Computing Formulas for Loop-Free Commands by Following Program Structure Forward VCG - Strongest Postconditions rules Backward VCG - Weakest Preconditions rules Continued in Lecture 04 text/html 2010-03-19T13:59:30+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_04?rev=1269003570&do=diff Lecture 04: Hoare Logic Rules. Symbolic Execution. Idea of Data-Flow Analysis Recall Lecture 03a Syntactic Rules for Hoare Logic - We derive syntactic rules that do not directly refer to semantics of commands as relations. Forward Symbolic Execution - How to combine program execution and strongest postconditions. text/html 2010-04-12T12:06:16+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_06?rev=1271066776&do=diff Lecture 06: Abstract Interpretation Background Control-Flow Graphs and While Theorem: How to convert a program to have a single loop. What does this mean about invariants? Loop invariant inference over a restricted set of invariants. Need for approximation. text/html 2010-04-16T01:19:21+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_07?rev=1271373561&do=diff Lecture 07: Abstract Interpretation Basics Continuing Lecture 06 We have seen in exercises Products of Lattices Abstract Interpretation of Transition System Collecting Semantics Galois Connection Using Galois Connection in Abstraction Interpretation Abstract Interpretation Recipe Variable Range Analysis for Example Program References * Principles of Program Analysis Book * Lecture notes on static analysis by Michael Schwartzbach (sections 4,5,6,7 in particular), and [pdf file] * … text/html 2010-04-20T11:55:45+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_08?rev=1271757345&do=diff Lecture 08: Convergence of Abstract Interpretation. Predicate Abstraction Idea of abstract interpretation: overapproximate computation in the lattice of sets of states Abstract Interpretation Recipe Mapping Fixpoints under Lattice Morphisms Comparing Fixpoints of Sequences Chaotic Iteration in Abstract Interpretation Termination of Abstract Interpretation Widening in Variable Range Analysis Continued in Lecture 09 References * Principles of Program Analysis Book * Lecture notes on … text/html 2010-04-20T11:56:42+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_09?rev=1271757402&do=diff Lecture 09: Widening. Predicate Abstraction Widening in Variable Range Analysis Abstract Interpretation with Conjunctions of Predicates Powerdomains for Finite Domains Powerset of Conjunctions of Predicates Analyses Based on Formulas Continued in Lecture 10 text/html 2010-05-03T09:57:49+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_10?rev=1272873469&do=diff Lecture 10: Quantifier Elimination, Partial Evaluation, and Synthesis [From Constraint Solving to Synthesis] Quantifier Elimination Basics Quantifier Elimination Definition QE from Conjunction of Literals Suffices Definition of Presburger Arithmetic QE for Presburger Arithmetic Synthesis Comfusy tool demo William Cook: Online Partial Evaluation of Model Interpreters Talk Video A reference on partial evaluation: Partial Evaluation and Automatic Program Generation A partial evaluation … text/html 2010-04-20T15:04:14+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_11?rev=1271768654&do=diff Lecture 11: Procedures: Semantics, Specifications, and Analysis Relational Semantics of Procedures Procedure Contracts and Their Meaning Reasoning about Procedures by Inlining Contracts Frame Conditions and Invariants Specification Variables and Data Abstraction Notion and Uses of Specification Variables Specification Variables for Public Interfaces Controlling When Invariants Hold Soundness of Simple Ghost Variables References on Interprocedural Analysis [Two Approaches to Interproce… text/html 2010-05-03T17:46:55+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_12?rev=1272901615&do=diff Lecture 12: More Quantifier Elimination. Small Models More on Integers Summary Example with Integers Recall: QE for Presburger Arithmetic Bounding Variables in Presburger Arithmetic Small Solutions for Quantifier-Free Presburger Arithmetic Small Models Classical Decision Problem Exists-Forall Class Definition Deciding Exists-Forall Class Continued in Lecture 13 text/html 2010-05-10T18:06:20+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_13?rev=1273507580&do=diff Lecture 13: Reasoning about Sets and Data Structures Continuing Lecture 12 Programs with References and Arrays Insertion into Doubly-Linked List Program Memory as Graph Language with Dynamic Allocation Semantics of Dynamic Object Allocation Semantics of Field Reads and Writes Semantics of Array Manipulations Assertions for Correct Use of Arrays and Heaps Simplification of Side Effecting Expressions FOL with Update Expressions Proving Programs with Dynamic Allocation Small Models App… text/html 2010-05-11T20:59:13+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_14?rev=1273604353&do=diff Lecture 14: Logics for Data Structures: BAPA and WS1S Continuing Lecture 13 BAPA Deciding Boolean Algebra with Presburger Arithmetic WS1S (Jahob demos for combination of SPASS, MONA, BAPA to prove ListSize.java Need for Reachability Weak Monadic Logic of One Successor References * [Languages, Automata, and Logic, by Wolfgang Thomas] * The MONA Project Continued in Lecture 15 text/html 2010-05-17T13:44:56+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_15?rev=1274096696&do=diff Lecture 15: Decision Procedure for WS1S Weak Monadic Logic of One Successor Review Strings and languages Finite state machine Determinization of finite state machine Finite state machine with epsilon transitions Closure properties of finite state machines Regular expression Equivalence of finite state machine and regular expression languages Connection between WS1S and Automata Regular expressions for automata with parallel inputs Using Automata to Decide WS1S Remarks on WS1S Comple… text/html 2010-05-25T10:32:47+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_16?rev=1274776367&do=diff Lecture 16 Continuing WS1S Continuing Lecture 15 Using Automata to Decide WS1S Remarks: * Remarks on WS1S Complexity * Expressing finite automata in MSOL over strings ListReverse.java WS2S Tree automata References * Logic and Automata Theory Course * [Languages, Automata, and Logic, by Wolfgang Thomas] * Tree Automata Techniques and Applications (Tata book) * The MONA Project * Timbook for Reachability Analysis and Tree Automata Calculations * [Decidability of Second-Or… text/html 2010-05-25T17:22:10+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_17?rev=1274800930&do=diff Lecture 17: Tree Automata. Semantics of Procedures Encoding n-ary trees into binary trees WS2S Tree automata Procedures Language with Specified Procedures Review: Relational Semantics Relational Semantics of Procedures References * Logic and Automata Theory Course * [Languages, Automata, and Logic, by Wolfgang Thomas] * Tree Automata Techniques and Applications (Tata book) * The MONA Project * Timbook for Reachability Analysis and Tree Automata Calculations * [Decidability o… text/html 2010-05-31T10:13:33+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_18?rev=1275293613&do=diff Lecture 18: Reasoning about Specified Procedures Relational Semantics of Procedures Procedure Contracts and Their Meaning Reasoning about Procedures by Inlining Contracts Frame Conditions and Invariants Specification Variables Specification Variables with Definitions: ListReverse.java Ghost Specification Variables: CursorList.java * variables that are under user * public and private invariants * specifying simple iterators text/html 2010-06-03T19:14:20+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_19?rev=1275585260&do=diff Lecture 19: Some Approaches to Automated Interprocedural Analysis Continuing Lecture 18 Describing Systems Trace Semantics Example with Procedures Describing Specifications Temporal Logic Subset as WS1S Fragment Checking that Systems Conform to Specifications Transforming Temporal Specifications into Contracts Run-Time Monitoring Model Checking Finite State Systems Model Checking Systems with Procedures Reachable pushdown configurations are regular text/html 2010-11-17T22:12:31+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/lecture_20?rev=1290028351&do=diff Set Constraints Interconvertibility of a class of set constraints and context-free-language reachability Definition of Set Constraints Set Constraints for Algebraic Datatype Inference Solving Set Constraints using Monadic Class More on set constraints: * [Set Constraints with Projections] (are NEXPTIME complete), JACM 2010 * Introduction to set constraint-based analysis * [Practical aspects of set based analysis] * Banshee * The complexity of set constraints * [Bachmair, Ganzin… text/html 2010-05-21T02:42:02+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/listreverse.java?rev=1274402522&do=diff List Reversal in Jahob /* Shows how fast things are when vc is given on the folklore example. Also, Bohne can infer the invariants. */ public final class Node { public /*: claimedby List */ Node next; public /*: claimedby List */ int data; } public class List { private static Node first; /*: private static specvar next_star :: "obj => obj => bool"; private vardefs "next_star == (% a b. (a,b) : {(x, y). x..Node.next = y}^*)"; public static specvar… text/html 2010-05-11T21:05:09+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/listsize.java?rev=1273604709&do=diff List.java // Program that uses first-order reasoning, reachability, and cardinality bounds class List { private List next; private Object data; private static List root; private static int size; /*: private static specvar nodes :: objset = "{}"; public static specvar content :: objset = "{}"; vardefs "nodes == {n. n \<noteq> null \<and> (root,n) \<in> {(u,v). u..next=v}^*}"; vardefs "content == {x.\<exists>n. x=n..data \<and> n \<in> nodes}"; invariant sizeIn… text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/model_checking_finite_state_systems?rev=1429630462&do=diff Model Checking Finite-State Systems Suppose we have a finite state system given by an automaton , compile the specification into an automaton and check , that is that is, check that the product of automata and accepts no strings (each string would be a counterexample). text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/model_checking_systems_with_procedures?rev=1429630462&do=diff Model Checking Systems with Procedures Suppose we have a system given by a context-free grammar and a specification given by a regular language . System meets the specification iff , that is Note: * is a regular language * is also a regular language text/html 2010-04-12T13:49:53+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/principles_of_program_analysis_book?rev=1271072993&do=diff Principles of Program Analysis F. Nielson, H.R. Nielson, C. Hankin: Principles of Program Analysis, Springer, 1999 * Authors' Page * Google Books * SLIDES * System to Build Analyzers text/html 2010-05-28T01:57:46+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/priorityqueueannot.java?rev=1275004666&do=diff public /*: claimedby PriorityQueue */ class PriorityQueueElement { public Object ob; public int key; } public class PriorityQueue { private PriorityQueueElement[] queue; private int length; /*: public specvar init :: bool = "False"; public specvar content :: "(obj * int) set"; public specvar smaxlen :: int; public specvar slength :: int; specvar spqueue :: "obj set"; vardefs "init == (queue \<noteq> null)"; vardefs "spqueue == {p.… text/html 2010-05-31T15:00:13+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/run-time_monitoring?rev=1275310813&do=diff Run-Time Monitoring Take a program (infinite state) and automaton for specification , and run both and in parallel. reports an error if it gets into a state from which it cannot reach an accepting state. Advantage: works for infinite-state systems, and for very expressive specifications text/html 2010-05-31T14:53:12+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/safety_temporal_logic_as_ws1s_fragment?rev=1275310392&do=diff A Temporal Logic Subset as WS1S Fragment Overview In linear temporal logic there is an implicit notion of time. Just like quantifiers update the environment with the variable over which they quantify, temporal operators update this implicitly named variable. The notion of implicitly named variables is also a feature of text/html 2010-03-04T21:26:01+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/simple_sat_solver?rev=1267734361&do=diff Simple SAT Solver Written by Hossein Hojjat object DPLL { case class Literal(val name: String, val pos: Boolean) def negate(l : Literal) = Literal(l.name, !l.pos) type Clause = Set[Literal] def DPLL(f : Set[Clause]) : (Boolean,Map[String,Boolean]) = { if(f.isEmpty) return (true,Map.empty[String,Boolean]) if(f.exists(clause => clause.isEmpty)) return (false,Map.empty[String,Boolean]) if(f.exists(clause => clause.size == 1)) { val unit_clause: Literal = f.find(clause =… text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/summary_example_with_integers?rev=1429630462&do=diff Summary Example with Integers var a = new Array[Int](2*N) var i = 0 while // loop invariant: 0 <= i && i <= N (i < N) { a[2*i] = 0 a[2*i+1] = 1 i = i + 1 } We can show that the invariant is preserved and that the invariant implies that there are no array out of bounds errors. text/html 2010-12-09T18:14:11+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/top?rev=1291914851&do=diff Synthesis, Analysis, and Verification 2010 Next edition: Synthesis, Analysis, and Verification 2011 Course Information * Course in the Catalog * 2009 Edition * 2008 Edition Moodle Page for Homework Submission Course Material Week 01, February 22 * Lecture 01 * Exercises 01 in INM10 * Homework 01 * Some relevant easy reading, from CACM: * A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World * Retrospective: An Axiomatic Basis for Compu… text/html 2015-04-21T17:34:22+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/trace_semantics?rev=1429630462&do=diff Trace Semantics One way to describe the meaning of the program is to give a relation between initial and final states, a set of pairs such that executing program from reaches the final state . Another way is to associate with a program a set of traces text/html 2010-05-31T15:19:14+0200 Anonymous (anonymous@undisclosed.example.com) https://lara.epfl.ch/w/sav10/transforming_temporal_specifications_into_contracts?rev=1275311954&do=diff Transforming Temporal Specifications into Contracts using Specification Variables During the verification of a program with procedures, when a procedure call is encountered, the procedure's contract is evaluated. We assume that the user has supplied the procedure contracts, although it may also be possible to infer contracts (especially the