LARA: Laboratory for Automated Reasoning and Analysis https://lara.epfl.ch/w/ 2026-04-04T04:56:37+0200 LARA: Laboratory for Automated Reasoning and Analysis https://lara.epfl.ch/w/ https://lara.epfl.ch/w/lib/tpl/epflv2/images/favicon.ico text/html 2011-10-29T16:06:01+0200 Anonymous (anonymous@undisclosed.example.com) alin https://lara.epfl.ch/w/alin?rev=1319897161&do=diff Abortable Linearizable Objects text/html 2007-07-13T14:45:09+0200 Anonymous (anonymous@undisclosed.example.com) alloy_in_jahob https://lara.epfl.ch/w/alloy_in_jahob?rev=1184330709&do=diff This project consists in finding and implementing a mapping that permits generation of Alloy models from Jahob's datatype. The goal is to construct a bug finder based on SAT by coupling Alloy to Jahob. Project code Code Report Report text/html 2008-03-18T14:17:41+0200 Anonymous (anonymous@undisclosed.example.com) bank_account_example_in_jahob https://lara.epfl.ch/w/bank_account_example_in_jahob?rev=1205846261&do=diff Bank account example in Jahob Below is a simplistic global bank account with two balance fields. You can also download the example: The command to verify this example is ../../bin/jahob.opt Account.java -class Account -usedp cvcl and requires an SMT-LIB solver under the name 'cvcl' to be installed to work (download text/html 2011-02-10T23:14:27+0200 Anonymous (anonymous@undisclosed.example.com) bapa https://lara.epfl.ch/w/bapa?rev=1297376067&do=diff BAPA Resources More to come soon. See our publications on BAPA at lara.epfl.ch . See here on non-redudandant integer cones. text/html 2015-04-21T17:45:01+0200 Anonymous (anonymous@undisclosed.example.com) cartesianproducts https://lara.epfl.ch/w/cartesianproducts?rev=1429631101&do=diff Of the use of cartesian products... The purpose of this page is to summarize the current status of our plans on how to proceed with verification of PM expressions. Using sets Types Sets are convenient to represent type. We will always consider a type T to be represented by the corresponding set text/html 2025-02-17T20:54:06+0200 Anonymous (anonymous@undisclosed.example.com) cc https://lara.epfl.ch/w/cc?rev=1739822046&do=diff Computer Language Processing ---------- Spring 2025 page is here: <https://gitlab.epfl.ch/lara/cs320/> ---------- Examples of old course pages: * Fall 2022 * Fall 2021 * Fall 2020 text/html 2009-09-15T23:27:13+0200 Anonymous (anonymous@undisclosed.example.com) cc09 https://lara.epfl.ch/w/cc09?rev=1253050033&do=diff Were you looking for the page for the Compiler Construction course given in 2009? It's right here. text/html 2011-09-24T22:20:35+0200 Anonymous (anonymous@undisclosed.example.com) cc11 https://lara.epfl.ch/w/cc11?rev=1316895635&do=diff Redirect You probably meant to go to top. text/html 2012-10-09T16:59:13+0200 Anonymous (anonymous@undisclosed.example.com) cc12labs_04 https://lara.epfl.ch/w/cc12labs_04?rev=1349794753&do=diff Labs 04 This week and the next one, you'll work on the second part of the Tool compiler project. Your goal is to manually implement a recursive-descent parser to transform programs described by the Tool grammar into Abstract Syntax Trees. You also need to write a pretty-printer for these trees. This assignment is rather long and we can only recommend that you start early, that you make sure you understand every step, and that you ask otherwise. text/html 2009-06-05T22:03:38+0200 Anonymous (anonymous@undisclosed.example.com) ccost https://lara.epfl.ch/w/ccost?rev=1244232218&do=diff <http://richmodels.epfl.ch> text/html 2013-05-09T20:11:34+0200 Anonymous (anonymous@undisclosed.example.com) cfm https://lara.epfl.ch/w/cfm?rev=1368123094&do=diff Communications in Formal Methods * 5 pages in this 2-column format (local copy here) * Using arxiv.org for submission and permanent storage * Continuous submission * Peer reviewed using continuous review process * Experimental data uploaded and stored * Authors retain copyright. Creative commons license. text/html 2007-06-20T01:28:30+0200 Anonymous (anonymous@undisclosed.example.com) chord_notes https://lara.epfl.ch/w/chord_notes?rev=1182295710&do=diff What is a data race? Happens before. In lock-based programs. Approximating whether there can be a race at two accesses: * locations disjoint * locks same - unsound approximation in absence of must analysis (“unlikely races”) * locations same, then locks same (conditional may alias analysis) text/html 2012-01-24T17:51:58+0200 Anonymous (anonymous@undisclosed.example.com) circuits https://lara.epfl.ch/w/circuits?rev=1327423918&do=diff Synthesis of Sequential Circuits from Regular Trace Specifications text/html 2012-04-17T14:16:32+0200 Anonymous (anonymous@undisclosed.example.com) cisy https://lara.epfl.ch/w/cisy?rev=1334664992&do=diff Circuit-Based Synthesis from Regular Specifications See the paper Synthesis for Unbounded Bitvector Arithmetic. Until this page is updated, please contact Andrej Spielmann. Related project: RegSy and Comfusy. text/html 2008-09-17T09:19:39+0200 Anonymous (anonymous@undisclosed.example.com) closure_properties_of_finite_state_machines https://lara.epfl.ch/w/closure_properties_of_finite_state_machines?rev=1221635979&do=diff Closure properties of finite state machines If we have some number of finite state machines, we show how to create a finite state machine whose language is union, intersection, complement, concatenation, or iteration of the languages of these state machines. text/html 2015-07-20T20:17:28+0200 Anonymous (anonymous@undisclosed.example.com) clp https://lara.epfl.ch/w/clp?rev=1437416248&do=diff Computer Language Processing Computer Language Processing 2015 text/html 2007-08-16T15:19:37+0200 Anonymous (anonymous@undisclosed.example.com) codefromscala https://lara.epfl.ch/w/codefromscala?rev=1187270377&do=diff Code examples extracted from the scala libraries/compiler Here is a collection from pattern matching expressions found in the scala libraries, or in the compiler. Many of them are of limited interest, but could be used later on for suggesting improvements on verifiability, for examples by adding invariants and the like. Note that there are many more examples to be found there, but most of them were not collected, because they fell in one of the following patterns: text/html 2012-08-15T16:02:22+0200 Anonymous (anonymous@undisclosed.example.com) collaboration https://lara.epfl.ch/w/collaboration?rev=1345039342&do=diff LARA Collaboration Collaborating groups: * SAAR group, Max-Planck Institute for Software Systems * Programming Methods Lab, EPFL * Distributed Programming Laboratory, EPFL * Rupak Majumdar's group, Max-Planck Institute for Software Systems * ARGO, University of Belgrade * Darko Marinov's group, UIUC * Data Lab, EPFL Past members and longer-term visitors: text/html 2012-05-12T13:11:38+0200 Anonymous (anonymous@undisclosed.example.com) comfusy-examples https://lara.epfl.ch/w/comfusy-examples?rev=1336821098&do=diff COMFUSY: COMplete FUnctional SYnthesis - Examples * ScaleWeights import synthesis.Definitions._ object ScaleWeights { def main(args: Array[String]): Unit = { println("Give me a weight: ") val weight: Int = Console.readInt try { val (w1,w2,w3,w4) = choose((w1:Int,w2:Int,w3:Int,w4:Int) => ( w1 + 3 * w2 + 9 * w3 + 27 * w4 == weight && -1 <= w1 && w1 <= 1 && -1 <= w2 && w2 <= 1 && -1 <= w3 && w3 <= 1 && -1 <= w4 && w4 <= 1 )… text/html 2013-10-16T18:27:10+0200 Anonymous (anonymous@undisclosed.example.com) comfusy https://lara.epfl.ch/w/comfusy?rev=1381940830&do=diff COMFUSY: COMplete FUnctional SYnthesis Comfusy is a tool for synthesizing executable code from specifications in linear integer arithmetic and constraints on sets of objects. * see PLDI 2010 Paper for the description of this work Comfusy works as a plugin for the text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) complexity https://lara.epfl.ch/w/complexity?rev=1429630357&do=diff Complexity of the verification process Preliminary remarks Terminology * We say that two patterns have the same signature if, without their (optional) guard, they are identical. * The set of pattern is assumed to be the cartesian product representing the set of inputs that a pattern would match. text/html 2013-03-14T09:38:13+0200 Anonymous (anonymous@undisclosed.example.com) confdesk-notes https://lara.epfl.ch/w/confdesk-notes?rev=1363250293&do=diff Useful Links Play * Play * <http://www.playframework.com/> * <http://www.playframework.com/documentation/2.0/ScalaAnorm> JDBC * JDBC tutorial: <http://zetcode.com/db/postgresqljavatutorial/> DB Web Interface - For Direct Control over DB * <http://www.sql-workbench.net/downloads.html> (Java) * <http://isql.sourceforge.net/> (Java) * <http://mywebsql.net/> (PHP) * <http://sourceforge.net/projects/sqlshell/files/> (Java, command Line) * <http://henplus.sourceforge.net/> … text/html 2014-09-15T00:16:25+0200 Anonymous (anonymous@undisclosed.example.com) confdesk https://lara.epfl.ch/w/confdesk?rev=1410732985&do=diff ConfDesk: Coming Soon! See <http://slickchair.github.io/SlickChair/> text/html 2008-06-30T23:13:36+0200 Anonymous (anonymous@undisclosed.example.com) conferences https://lara.epfl.ch/w/conferences?rev=1214860416&do=diff Upcoming Conference Deadlines * VMCAI papers: August 22, 2008, <http://cs.uni-muenster.de/vmcai09/index.php> * PLDI papers: November 7, 2008, <http://www-plan.cs.colorado.edu/~pldi09/> * ETAPS abstracts: November 2, 2008, <http://www.cs.york.ac.uk/etaps09/> * CADE 2009, ?, <http://www.cs.mcgill.ca/~bpientka/cade09/> * LICS 2009, ?, <http://www.cl.cam.ac.uk/~amp12/> LARA Papers in Progress * Theories Sharing Sets * Online Static Analysis text/html 2007-06-21T15:36:21+0200 Anonymous (anonymous@undisclosed.example.com) constraint_based_analysis_of_java_using_jahob_and_amrc https://lara.epfl.ch/w/constraint_based_analysis_of_java_using_jahob_and_amrc?rev=1182432981&do=diff Constraint based analysis of java using jahob and amrc Project Introduction In this project, we are trying to bridge two verification tools Jahob and Armc. Jahob is quite powerful in accepting complecated Java programs and translate it into simplified intermidiate language. We are trying to write a translater from this representation of program to input format of ARMC. ARMC takes transition relation as input. ARMC is powerful in computing loop invariant and fixedpoint analysis automaticlly. Re… text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) context-free_grammars https://lara.epfl.ch/w/context-free_grammars?rev=1429630357&do=diff Context-Free Grammars Purpose and Expressive Power A context-free grammar is a way to specify languages. Context-free grammars are more powerful than regular expressions: for each regular expression there is an equivalent context-free grammar, but the converse need not hold. Context-free grammars supposed not just iteration like regular expressions, but also more general forms of recursion. text/html 2007-04-15T18:40:02+0200 Anonymous (anonymous@undisclosed.example.com) correctness_of_formula_propagation https://lara.epfl.ch/w/correctness_of_formula_propagation?rev=1176655202&do=diff Correctness of formula propagation By definition of sp and our requirements of N, the propagation is correct for code without loops. Using an example of a single loop, we explain that if the analysis terminates then it computes an inductive invariant weaker than the initial formula. text/html 2008-08-22T17:53:52+0200 Anonymous (anonymous@undisclosed.example.com) cost-cert https://lara.epfl.ch/w/cost-cert?rev=1219420432&do=diff Please see the new page. text/html 2015-12-02T11:04:49+0200 Anonymous (anonymous@undisclosed.example.com) cvc4-synthesis https://lara.epfl.ch/w/cvc4-synthesis?rev=1449050689&do=diff Synthesis within CVC4 Counterexample Guided Quantifier Instantiation for Synthesis in SMT We provide the following supplementary material for this paper. Solver The zip archive containing the binary of CVC4 used in our experiments can be found here: cvc4-sygus.zip * Configuration cvc4+sg from the paper is enabled by command line parameters text/html 2015-05-24T17:24:24+0200 Anonymous (anonymous@undisclosed.example.com) cvc4 https://lara.epfl.ch/w/cvc4?rev=1432481064&do=diff CVC4 SMT Solver The CVC4 SMT solver is available from <http://cvc4.cs.nyu.edu> Information on experiments with synthesis within CVC4 is available on the cvc4-synthesis page. text/html 2009-08-11T00:37:53+0200 Anonymous (anonymous@undisclosed.example.com) data_structure_examples.html https://lara.epfl.ch/w/data_structure_examples.html?rev=1249943873&do=diff Examples of Data Structures Verified in Jahob [Array.java] [Association.java] [BinarySearchTree.java] [CursorList.java] [CircularList.java] [Hashtable.java] [PriorityQueue.java] [SinglyLinkedList.java] For screen shots and a comparison with the Sun Java library interface for ArrayList.java, see the following older version of our benchmarks. text/html 2007-05-05T17:21:14+0200 Anonymous (anonymous@undisclosed.example.com) determinization_of_finite_state_machine https://lara.epfl.ch/w/determinization_of_finite_state_machine?rev=1178378474&do=diff Determinization of finite state machine For every finite state machine there exists a deterministic finite state machine that accepts the same language. This machine is given by where * * . The corresponding deterministic state machine maintains a set of states instead of just one state, and simultaneously transitions into all states that the original machine could reach from the current set of states. text/html 2013-02-20T14:34:52+0200 Anonymous (anonymous@undisclosed.example.com) dp https://lara.epfl.ch/w/dp?rev=1361367292&do=diff Progress in Decision Procedures: from Formalizations to Applications What we will need from participants: * name, web page, short biography (up to 300 words), photo * if presenting: title and abstract (up to 500 words) of the talk * arrival and departure times text/html 2014-09-23T17:16:12+0200 Anonymous (anonymous@undisclosed.example.com) eldarica https://lara.epfl.ch/w/eldarica?rev=1411485372&do=diff ELDARICA ---------- NEW: GitHub link: <https://github.com/uuverifiers/eldarica> ---------- [ ] A real Eldarica Tree A reachability tree created by Eldarica for the mutual exclusion protocol with arbitrary number of clients Eldarica Eldarica is a predicate abstraction engine. It generates the abstract reachability tree (ART) using lazy abstraction with Cartesian abstraction. It uses the text/html 2008-05-15T13:01:50+0200 Anonymous (anonymous@undisclosed.example.com) encoding_lists_using_msol_over_strings https://lara.epfl.ch/w/encoding_lists_using_msol_over_strings?rev=1210849310&do=diff Encoding lists using MSOL over strings Example file 'MONA' tool: How to encode multiple lists How to encode * doubly-linked lists * cyclic lists: <http://lara.epfl.ch/~kuncak/jahob/ds/CircularList/> References * Verification via structure simulation * Field constraint analysis * Pointer Assertion Logic Engine text/html 2010-12-25T22:08:27+0200 Anonymous (anonymous@undisclosed.example.com) epfl_internships https://lara.epfl.ch/w/epfl_internships?rev=1293311307&do=diff Internships at EPFL Laboratory for Automated Reasoning and Analysis rarely accepts internships. Information about EPFL internships can be found here: * General Internship Applications (including applications from Europe and North America) * Special Internships program for students from India: all internship applications from India should proceed through this program text/html 2008-09-23T21:09:02+0200 Anonymous (anonymous@undisclosed.example.com) equivalence_of_finite_state_machine_and_regular_expression_languages https://lara.epfl.ch/w/equivalence_of_finite_state_machine_and_regular_expression_languages?rev=1222196942&do=diff Equivalence of finite state machines and regular expression languages We next show that a language is given by a regular expression if and only if it is a language of some finite state machine. If a language is given by one of these two ways, we can always convert to the other if this is more convenient. text/html 2007-03-30T20:45:43+0200 Anonymous (anonymous@undisclosed.example.com) equivalence_relation https://lara.epfl.ch/w/equivalence_relation?rev=1175280343&do=diff Equivalence relation An equivalence relation is a binary relation on set (that is, a subset of ) that is reflexive, symmetric, and transitive, that is, the following three properties hold: * * * Given an equivalence relation , we define the set of equivalence classes text/html 2008-06-05T17:11:45+0200 Anonymous (anonymous@undisclosed.example.com) exchanges_for_epfl_students https://lara.epfl.ch/w/exchanges_for_epfl_students?rev=1212678705&do=diff Exchange Programs for EPFL Students If you are an EPFL student, you may decide to explore an internship or master's thesis outside EPFL while being supervised by an EPFL faculty. Before deciding whether to visit, I advise a student to fully familiarize themselves with the work done both at EPFL and any other instututions that they are interested in visiting. text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) expressing_finite_automata_in_msol_over_strings https://lara.epfl.ch/w/expressing_finite_automata_in_msol_over_strings?rev=1429630357&do=diff Expressing finite automaton in WS1S Consider a finite automaton with alphabet , states , transition relation , initial state and final states . Let the sets denote the encoding of input string of the automaton. There exists an execution of an automaton iff there exist the intermediate states given by transition relation text/html 2007-05-06T21:04:33+0200 Anonymous (anonymous@undisclosed.example.com) expressing_regular_expressions_in_msol_over_strings https://lara.epfl.ch/w/expressing_regular_expressions_in_msol_over_strings?rev=1178478273&do=diff Expressing regular expressions in MSOL over strings Idea: for each regular expression of a automaton for parallel inputs associate a formula with free variables such that is valid precisely for whose sets of numbers for which * and are singletons * the strings given by the parts of text/html 2007-06-29T21:15:52+0200 Anonymous (anonymous@undisclosed.example.com) expressive_power_of_a_fragment_of_ws1s https://lara.epfl.ch/w/expressive_power_of_a_fragment_of_ws1s?rev=1183144552&do=diff [Expressive Power of a Fragment of WS1S] text/html 2009-04-28T20:05:52+0200 Anonymous (anonymous@undisclosed.example.com) finite_state_machine https://lara.epfl.ch/w/finite_state_machine?rev=1240941952&do=diff Finite state machine A finite state machine is a way of defining a language (see Strings and languages). We give a string to the machine, which examines the string one character by one, and at the end decides whether the string is the language or not. A non-deterministic finite state machine text/html 2008-05-14T10:22:04+0200 Anonymous (anonymous@undisclosed.example.com) finite_state_machine_with_epsilon_transitions https://lara.epfl.ch/w/finite_state_machine_with_epsilon_transitions?rev=1210753324&do=diff Finite state machine with epsilon transitions Definition Finite state machine with epsilon transitions is an extension of a finite state machine where transitions can be labelled by . If such a transition exists then an automaton may transition from to without consuming any portion of the input string. text/html 2011-05-06T19:08:08+0200 Anonymous (anonymous@undisclosed.example.com) fmcad https://lara.epfl.ch/w/fmcad?rev=1304701688&do=diff Cooperation Status and Publication of FMCAD Proceedings Panagiotis Email ACM Getting in-cooperation status, see here: <http://cms.acm.org/incoop/cms_incoop.cfm> * fill in General Conference Information, * upload a copy of the sponsoring organization's Certificate of Insurance (COI) or a Financial Responsibility Letter on the Sponsoring Organization Letterhead, text/html 2011-08-25T00:28:23+0200 Anonymous (anonymous@undisclosed.example.com) fmcad11 https://lara.epfl.ch/w/fmcad11?rev=1314224903&do=diff FMCAD 2011 Instructions for Camera-Ready Version of Papers <http://www.cs.utexas.edu/users/ragerdl/fmcad11/> Congratulations on the acceptance of your FMCAD 2011 contribution. We are pleased to inform you that we expect the proceedings to be published both through ACM and IEEE digital libraries (as well as on the FMCAD web site for rapid dissemination). text/html 2011-08-14T12:12:11+0200 Anonymous (anonymous@undisclosed.example.com) fmcad11a https://lara.epfl.ch/w/fmcad11a?rev=1313316731&do=diff IEEE Requirements For the final version you will need to follow the steps below. More information will be available down the line, so please be prepared to revise the submission after the deadline, once the details of the IEEE publication become available. We apologize for the inconvenience. For the original deadline, please just try to do your best and embed the fonts. text/html 2013-11-21T21:00:46+0200 Anonymous (anonymous@undisclosed.example.com) fmcad2014 https://lara.epfl.ch/w/fmcad2014?rev=1385064046&do=diff FMCAD 2014 Information Page Formal Methods in Computer-Aided Design 2014, 21-24 October 2014 * collocated and sharing tutorials with MEMOCODE 2014, 19-21 October 2014 Conference Google Calendar: * HTML, XML, ICAL (.ics) Updates About Lausanne * Short Video Local Information text/html 2014-11-04T11:50:33+0200 Anonymous (anonymous@undisclosed.example.com) formal https://lara.epfl.ch/w/formal?rev=1415098233&do=diff Formal Methods @ EPFL EPFL conducts research in formal methods, focusing on tools and algorithms for construction of reliable and efficient software and hardware: * Automated Reasoning and Analysis Lab * Barbara Jobstmann * Communications and Applications Laboratory * Data Analysis Theory and Applications Laboratory * Dependable Systems Lab * Distributed Programming Laboratory * Embedded Systems Laboratory * Integrated Systems Laboratory * Processor Architecture Laboratory *… text/html 2009-11-18T22:23:21+0200 Anonymous (anonymous@undisclosed.example.com) functionalsynthesis https://lara.epfl.ch/w/functionalsynthesis?rev=1258579401&do=diff Functional Synthesis Paper. Lib. Plugin. Z3. text/html 2019-09-18T11:01:16+0200 Anonymous (anonymous@undisclosed.example.com) funding https://lara.epfl.ch/w/funding?rev=1568797276&do=diff LARA Funding EPFL Laboratory for Automated Reasoning and Analysis is supported by the funding from * EPFL School of Computer and Communication Sciences * Swiss National Science Foundation Past funding support includes: * European Research Council (ERC), which funded the Implicit Programming project * Microsoft Innovation Cluster for Embedded Software * European Cooperation in Science and Technology text/html 2021-10-29T19:04:42+0200 Anonymous (anonymous@undisclosed.example.com) fv https://lara.epfl.ch/w/fv?rev=1635527082&do=diff EPFL Course: Formal Verification, CS-550 ---------- The 2021 onwards page: <https://gitlab.epfl.ch/lara/cs550/> ---------- Old pages: Formal Verification 2020, Formal Verification 2019, and other web pages from 2008 onwards with hidden gems of wisdom. text/html 2019-12-09T22:58:20+0200 Anonymous (anonymous@undisclosed.example.com) fvquimsical https://lara.epfl.ch/w/fvquimsical?rev=1575928700&do=diff Some Verification-Related Quizzes 2015 <https://lara.epfl.ch/w/_media/sav17/quiz_solutions2015.pdf> 2013 <https://lara.epfl.ch/w/_media/sav17/quiz_solutions2013.pdf> 2012 * <https://lara.epfl.ch/w/_media/sav13/quiz_2012.pdf> * <https://lara.epfl.ch/w/_media/sav13/quiz_solutions_2012.pdf> 2011 * [Quiz 1] * [Quiz 2] 2010 * [Quiz 1] * [Quiz 2] text/html 2008-02-18T12:53:26+0200 Anonymous (anonymous@undisclosed.example.com) gallier_logic_book https://lara.epfl.ch/w/gallier_logic_book?rev=1203335606&do=diff Gallier's Logic Book There are many textbooks that cover propositional and first-order logic, its syntax, semantics, and proof theory. This Jean Gallier's book is available online and contains a lot of relevant material. You should not assume that you can quickly read through all of it. The most important sections are: text/html 2010-02-22T11:34:20+0200 Anonymous (anonymous@undisclosed.example.com) harrison_textbook https://lara.epfl.ch/w/harrison_textbook?rev=1266834860&do=diff Handbook of Practical Logic and Automated Reasoning by John Harrison (Intel Corporation, Portland, Oregon) * Cambrige University Press Site * author's resources text/html 2013-03-06T15:49:02+0200 Anonymous (anonymous@undisclosed.example.com) horn-nonrec-benchmarks https://lara.epfl.ch/w/horn-nonrec-benchmarks?rev=1362581342&do=diff Non-Recursive Horn Benchmarks * Horn constraints generated by Eldarica, output by Princess * Benchmarks are in SMT-LIB 2.0 and can be processes by e.g. Z3 Horn Clause Type Number of Benchmarks Download General 541 1.6 MB Head-Disjoint 991 2.5 MB Linear text/html 2013-11-22T15:41:07+0200 Anonymous (anonymous@undisclosed.example.com) horn-parametric-benchmarks https://lara.epfl.ch/w/horn-parametric-benchmarks?rev=1385131267&do=diff Parametric Timed Automata Benchmarks * Horn constraints generated by Eldarica for parametric timed automata benchmarks * Benchmarks are in SMT-LIB 2.0 and can be processes by e.g. Z3 Safe Benchmarks Unsafe Benchmarks text/html 2008-12-05T21:15:02+0200 Anonymous (anonymous@undisclosed.example.com) htmldoc https://lara.epfl.ch/w/htmldoc?rev=1228508102&do=diff htmldoc Here is an example use of htmldoc use to create a pdf file for the lectures. htmldoc --book --nup 2 -f lecture12.pdf \ http://lara.epfl.ch/dokuwiki/doku.php?id=compilation:applications_of_data-flow_analysis \ http://lara.epfl.ch/dokuwiki/doku.php?id=compilation:concrete_execution_as_data-flow_analysis \ http://lara.epfl.ch/dokuwiki/doku.php?id=compilation:designing_correct_data-flow_analyses \ http://lara.epfl.ch/dokuwiki/doku.php?id=compilation:termination_of_data-flow_analys… text/html 2016-11-18T10:43:33+0200 Anonymous (anonymous@undisclosed.example.com) impro https://lara.epfl.ch/w/impro?rev=1479462213&do=diff IMPLICIT PROGRAMMING Implicit programming is a proposed software development paradigm that aims to address longstanding bottlenecks of software construction. The problem that we address is obvious to anyone who has ever written a program: programming is harder than it should be text/html 2008-02-04T16:32:09+0200 Anonymous (anonymous@undisclosed.example.com) inheritance https://lara.epfl.ch/w/inheritance?rev=1202139129&do=diff A Guide To Inheritance in Programming Languages Inheritance is one of the core features of Object Oriented programming, which provides reusability and extensiblity. The use of inheritance is often debated among programmers, computer scientists, and language designers. Some claim it should be mostly avoided, and others - generally the functional programming community - go beyond it and advocate that it is simply a bad idea. One of the most common objections is pointed out in the module system s… text/html 2013-06-29T10:53:35+0200 Anonymous (anonymous@undisclosed.example.com) insynth https://lara.epfl.ch/w/insynth?rev=1372496015&do=diff InSynth: Type-Driven Interactive Synthesis of Code Snippets InSynth is a tool for interactive synthesis of code snippets. It synthesizes a ranked list of code fragments that use given library functions. A recent version is presented in the following paper: text/html 2007-06-21T15:56:29+0200 Anonymous (anonymous@undisclosed.example.com) interfaces_for_atomicity https://lara.epfl.ch/w/interfaces_for_atomicity?rev=1182434189&do=diff The project 'Interfaces for Atomicity' is based on recent work, mainly started with a type system for atomicity (<http://portal.acm.org/citation.cfm?id=781169&dl=ACM&coll=portal>). The current work tries to extend static analysis for atomicity for non-blocking programs(<http://portal.acm.org/citation.cfm?doid=1065944.1065953>). The presentation is [here.] The project aims at developing an assume-guarantee reasoning for atomicity of concurrent threads in a program. The idea is to capture the b… text/html 2007-03-20T17:59:44+0200 Anonymous (anonymous@undisclosed.example.com) interpreter https://lara.epfl.ch/w/interpreter?rev=1174409984&do=diff Interpreter An interpreter executes a given program. An interpreter can traverse the statements of the program, evaluate the expressions in the current state and update the values of the state in the presence of assignment statements. Interpreter is strongly related to a compiler, the difference being that the compiler first translates the code into the target language, which can then be executed, whereas interpreter directly executes the language. Therefore, both the compiler and interprete… text/html 2007-05-14T12:02:03+0200 Anonymous (anonymous@undisclosed.example.com) introduction_to_using_msol_over_strings_to_verify_linked_lists https://lara.epfl.ch/w/introduction_to_using_msol_over_strings_to_verify_linked_lists?rev=1179136923&do=diff Introduction to using MSOL over strings to verify linked data structures Here is a simple linked list operation in Jahob. What do verification conditions look like? tree [Node.next] --> F(Node.next) I will describe a decision procedure that can decide such formulas. text/html 2011-07-21T15:18:56+0200 Anonymous (anonymous@undisclosed.example.com) isynth https://lara.epfl.ch/w/isynth?rev=1311254336&do=diff InSynth Tool Please Click here for the InSynth website. text/html 2011-01-26T18:32:58+0200 Anonymous (anonymous@undisclosed.example.com) isynth_home https://lara.epfl.ch/w/isynth_home?rev=1296063178&do=diff Isynth text/html 2017-03-19T16:33:54+0200 Anonymous (anonymous@undisclosed.example.com) jahob_system https://lara.epfl.ch/w/jahob_system?rev=1489937634&do=diff Jahob Verification System Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints. text/html 2009-02-08T11:52:14+0200 Anonymous (anonymous@undisclosed.example.com) jahob_system_sets https://lara.epfl.ch/w/jahob_system_sets?rev=1234090334&do=diff Benchmarks for Set-Driven Combination of Logics and Verifiers * SizeList.java * SortedList.java * SizeDataTree.java * ThreadedTree.java For the description of the underlying technique, see the recent paper. For more information, see also the Jahob system text/html 2011-10-21T16:19:58+0200 Anonymous (anonymous@undisclosed.example.com) jniz3-scala-examples https://lara.epfl.ch/w/jniz3-scala-examples?rev=1319206798&do=diff Examples of Using Z3 with Scala Compiling and running the following examples requires that you obtain z3.jar, libz3.so (from Microsoft Research), and use Scala 2.8. The best way to figure out which functions to use is probably to read through the C API once, then through the Scala text/html 2011-08-03T14:37:18+0200 Anonymous (anonymous@undisclosed.example.com) jniz3 https://lara.epfl.ch/w/jniz3?rev=1312375038&do=diff Redirect See this page. text/html 2012-02-14T00:10:40+0200 Anonymous (anonymous@undisclosed.example.com) kaplan https://lara.epfl.ch/w/kaplan?rev=1329174640&do=diff Kaplan What is Kaplan? Kaplan is an extension of the Scala programming language that supports constraint-solving. Kaplan is described in the following paper: A.S. Köksal, V. Kuncak, P. Suter, Constraints as Control, POPL 2012, pp. 151-164. PDF Obtaining Kaplan text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) lambda_calculus https://lara.epfl.ch/w/lambda_calculus?rev=1429630357&do=diff Lambda calculus This is a very brief introduction to lambda calculus. Lambda calculus is a notation for defining functions. It is very simple and powerful. Two of its main uses are * foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala text/html 2011-02-10T23:02:55+0200 Anonymous (anonymous@undisclosed.example.com) lara https://lara.epfl.ch/w/lara?rev=1297375375&do=diff BAPA Resources text/html 2011-06-16T21:02:22+0200 Anonymous (anonymous@undisclosed.example.com) lara_posters https://lara.epfl.ch/w/lara_posters?rev=1308250942&do=diff LARA POSTERS Proglab Download it [here] Comfusy Available in [PDF]. The SVG source is on the SVN. Instructions to generate PDF from SVG are here. text/html 2018-11-01T16:12:04+0200 Anonymous (anonymous@undisclosed.example.com) laragit https://lara.epfl.ch/w/laragit?rev=1541085124&do=diff Using our Git Server Setup (If you don't know what an SSH public key is or don't know how to generate a key pair, your can read http://help.github.com/linux-set-up-git/ from GitHub. Just ignore all the parts that are specific to GitHub.) Note that you need to follow these steps for each computer than you plan to use. Also note that EPFL members that are not part of the lab (e.g. students) should the link text/html 2008-06-06T20:33:29+0200 Anonymous (anonymous@undisclosed.example.com) learning https://lara.epfl.ch/w/learning?rev=1212777209&do=diff Machine Learning Page * Charles Kemp's page * ILP * Workshop on Machine Learning at OSDI'08 * Multi-Relational Data Mining * MRDTL: A multi-relational decision tree learning algorithm text/html 2008-09-18T11:27:07+0200 Anonymous (anonymous@undisclosed.example.com) lecture16_transcript https://lara.epfl.ch/w/lecture16_transcript?rev=1221730027&do=diff NaturalLanguageProcessing-Lecture16 Instructor: (Christopher Manning) Okay, hi, everyone. So today I’m going to go through in some detail some of the ideas that I started on last week of how you can actually go about building a compositional semantic representation to provide some kind of handle on how you can start with meanings of words and some tactic structure, and actually put together a meaning for a complex sentence. And so most of the work that’s gonna be talked about here is how can… text/html 2015-02-06T13:52:26+0200 Anonymous (anonymous@undisclosed.example.com) leon-repair-benchmarks https://lara.epfl.ch/w/leon-repair-benchmarks?rev=1423227146&do=diff Leon System for Verification, Synthesis and Repair The following list of benchmarks were used to evaluate our repair system. Each benchmark contains a “fixme” comment indicating the place and kind of error introduced: * Desugar.desugar1 * Desugar.desugar2 * Desugar.desugar3 * Desugar.desugar4 * HeapSort.merge1 * text/html 2015-02-10T17:14:23+0200 Anonymous (anonymous@undisclosed.example.com) leon-repair https://lara.epfl.ch/w/leon-repair?rev=1423584863&do=diff Leon System for Verification, Synthesis and Repair The following list of benchmarks were used to evaluate our repair system. Each benchmark contains a “fixme” comment indicating the place and kind of error introduced: * Compiler.desugar1 * Compiler.desugar2 * Compiler.desugar3 * Compiler.desugar4 * Compiler.desugar5 text/html 2015-06-21T21:25:48+0200 Anonymous (anonymous@undisclosed.example.com) leon https://lara.epfl.ch/w/leon?rev=1434914748&do=diff Leon System for Verification, Synthesis and Repair [The One, Leon Way] Leon is an automated system for verifying, repairing, and synthesizing functional Scala programs. The system can be tried out online, with no installation required, at the following link: <http://leon.epfl.ch> Leon source code is publicly available on github: text/html 2008-12-05T18:38:37+0200 Anonymous (anonymous@undisclosed.example.com) lisp_seminar_nlp_2008 https://lara.epfl.ch/w/lisp_seminar_nlp_2008?rev=1228498717&do=diff Next Boston Lisp Meeting: Monday November 24th 2008 at 1800 at MIT 34-401B Gregory Marton will give a talk about the meanings of English words as programs. <http://fare.livejournal.com/136992.html> Gregory will introduce a way of thinking about the meanings of English words as programs (c.f. SHRDLU), cast the problem of language learning as a search through the space of possible programs, and show first steps in learning. Gregory has created a system called Sepia that makes it relatively easy t… text/html 2008-06-05T17:09:15+0200 Anonymous (anonymous@undisclosed.example.com) master_s_program https://lara.epfl.ch/w/master_s_program?rev=1212678555&do=diff Master Program in EPFL I&C School Master programs at our school offer an intensive program with courses an oportunities for research through semester and summer projects, and a possibility of specializations in several exciting areas. The program opens up many opportunities for graduated students, including PhD program at EPFL and other universities, as well as employment opportunities. text/html 2019-09-18T11:02:35+0200 Anonymous (anonymous@undisclosed.example.com) menu https://lara.epfl.ch/w/menu?rev=1568797355&do=diff <li><a href="http://lara.epfl.ch/w/Start">About</a><br/></li> <li><a href="http://lara.epfl.ch/w/Software">Software</a><br/></li> <li><a href="http://lara.epfl.ch/w/Teaching">Teaching</a><br/></li> <li><a href="http://lara.epfl.ch/w/Publications">Publications</a><br/></li> <li><a href="http://lara.epfl.ch/w/funding">Funding</a><br/></li> <li><a href="http://lara.epfl.ch/w/News">News</a><br/></li> text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) minimization_of_state_machines https://lara.epfl.ch/w/minimization_of_state_machines?rev=1429630357&do=diff Minimization of Deterministic Finite State Machines We consider deterministic finite state machine . Goal: build a state machine with the least number of states that accepts the language . * we obtain a space-efficient, executable representation of a regular language text/html 2007-04-24T15:34:51+0200 Anonymous (anonymous@undisclosed.example.com) monadic_second-order_logic_over_trees https://lara.epfl.ch/w/monadic_second-order_logic_over_trees?rev=1177421691&do=diff Monadic Second-Order Logic over Trees * Tree Automata Techniques and Applications (Tata book) * The MONA Project * Timbook for Reachability Analysis and Tree Automata Calculations text/html 2007-05-05T16:09:31+0200 Anonymous (anonymous@undisclosed.example.com) monoid https://lara.epfl.ch/w/monoid?rev=1178374171&do=diff Monoid Monoid is a triple where such that * is a semigroup and * is a neutral element for The second condition means that for all , text/html 2008-05-15T09:26:17+0200 Anonymous (anonymous@undisclosed.example.com) msol_over_strings https://lara.epfl.ch/w/msol_over_strings?rev=1210836377&do=diff MSOL over Strings Syntax and Semantics of Weak Monadic Second-Order Logic over Strings Explanation of the name: * second-order logic: we can quantify not only over elements but also over sets and relations * monadic: we cannot quantify over any relations, just unary relations, that is, sets text/html 2009-02-25T21:37:00+0200 Anonymous (anonymous@undisclosed.example.com) nenofar https://lara.epfl.ch/w/nenofar?rev=1235594220&do=diff Nenofar = Negation Normal Form Automated Reasoner [Nenuphar = Water Lily] Available downloads: * a Linux binary of Nenofar compiled statically against libstdc++ and libc : <http://lara.epfl.ch/~psuter/nenofar-dist/nenofar> * the compressed sources: <http://lara.epfl.ch/~psuter/nenofar-dist/nenofar.tgz> * the benchmarks: <http://lara.epfl.ch/~psuter/nenofar-dist/benchmarks.tgz> For more information: * Philippe Suter * Non-Clausal Satisfiability Modulo Theories (master's thesis by P… text/html 2017-03-15T10:01:23+0200 Anonymous (anonymous@undisclosed.example.com) news https://lara.epfl.ch/w/news?rev=1489568483&do=diff LARA NEWS (Partial List) See also the publications. ---------- 2012 * Implicit Programming project funded with a Starting ERC Grant * The second Rich Model Toolkit meeting of 2012 took place in Manchester * Andrej Spielmann presents Synthesis for Unbounded Bitvector Arithmetic at IJCAR 2012 * Giuliano Losa presents Speculative Linearizability at PLDI 2012 * The first Rich Model Toolkit meeting of 2012 took place in text/html 2011-12-14T14:42:16+0200 Anonymous (anonymous@undisclosed.example.com) nicg https://lara.epfl.ch/w/nicg?rev=1323870136&do=diff Non-Redundant Integer Cones - Resources This page describes our work on computing maximal non-redundant integer cone generators. The algorithms, implementations, and results are described in the following technical report: [Identifying Maximal Non-Redundant Integer Cone Generators] As part of this search we have also explicitly computed all non-redundant integer cones modulo row and column permutations: text/html 2015-04-21T17:50:33+0200 Anonymous (anonymous@undisclosed.example.com) non-converging_iteration_in_reals https://lara.epfl.ch/w/non-converging_iteration_in_reals?rev=1429631433&do=diff An example of a fixed point iteration not converging to a fixed point in one countable sequence (draw figure) Start from e.g. x=1/2. Obtain a series converging to 1, but 1 is not a fixed point because . This is because is not continuous. If it was continous (at least, continuous from the left), we would have the desired property. text/html 2008-10-26T22:00:45+0200 Anonymous (anonymous@undisclosed.example.com) note_on_buffer_overflows https://lara.epfl.ch/w/note_on_buffer_overflows?rev=1225054845&do=diff Note on Buffer Overflows A study published as a White Paper by Cisco Systems “Economic Impact of Network Security Threats”, describes virus Code Red, “Code Red (2001) The Code Red worm was a self-replicating malicious code that exploited a known vulnerability in Microsoft IIS servers. Code Red attempted to connect to TCP port 80 on a randomly chosen host. When a successful connection to port 80 was achieved, the attacking host sent an HTTP GET request to the victim, attempting to exploit a bu… text/html 2007-03-21T14:57:57+0200 Anonymous (anonymous@undisclosed.example.com) note_on_substitutions https://lara.epfl.ch/w/note_on_substitutions?rev=1174485477&do=diff On substitutions Let t1[x:=t0] denote the result of substituting all occurrences of variable x in term t1 with the term t0. These rules define substitution recursively: x[x:=t0] = t2 y[x:=t0] = y (for any variable y distinct from x) c[x:=t0] = c (for any constant symbol c) f(t1,...,tn)[x:=t0] = f(t1[x:=t0],...,tn[x:=t0]) text/html 2007-03-18T17:11:21+0200 Anonymous (anonymous@undisclosed.example.com) notes_on_context-free_grammars https://lara.epfl.ch/w/notes_on_context-free_grammars?rev=1174234281&do=diff Here is general information on Context-free Grammars. Typically, in a context-free grammar one can have multiple productions of the form N -> w1 N -> w2 M -> w3 M -> w4 M -> w5 I use the notation that corresponds to Backus-Naur form which collects all right-hand sides correspondig to same left-hand sides and separate the alternatives using the text/html 2007-04-04T17:01:50+0200 Anonymous (anonymous@undisclosed.example.com) ocaml_resources https://lara.epfl.ch/w/ocaml_resources?rev=1175698910&do=diff Ocaml Resources * The OCaml programming language: <http://caml.inria.fr/> is convenient for writing implementations for this class because of its support for algebraic data types and pattern matching, which makes dealing with abstract syntax trees easier. * <http://www.csc.villanova.edu/~dmatusze/resources/ocaml/ocaml.html> is a good crash-course in basic of OCaml. At the bottom of the file you are going to find pointers to the official OCaml manual and also to an introductory course given… text/html 2011-05-06T18:48:01+0200 Anonymous (anonymous@undisclosed.example.com) panagiotis_email https://lara.epfl.ch/w/panagiotis_email?rev=1304700481&do=diff Hi everyone, Here's a quick update with a quick overview of what needs doing for next year. Viktor, please feel free to contact me if you have question or run into trouble. The executive summary is that all permissions have been granted and now all that is left is for Hana to get the papers to the IEEE and ACM, so we're all set. text/html 2020-02-18T22:57:39+0200 Anonymous (anonymous@undisclosed.example.com) parcon https://lara.epfl.ch/w/parcon?rev=1582063059&do=diff EPFL CS-206: Parallelism and Concurrency Click Here for the For 2020 Edition of EPFL Course CS-206, Parallelism and Concurrency text/html 2009-03-26T17:12:17+0200 Anonymous (anonymous@undisclosed.example.com) partial_order https://lara.epfl.ch/w/partial_order?rev=1238083937&do=diff Partial Orders Partial ordering relation is a binary relation that is reflexive, antisymmetric, and transitive, that is, the following properties hold for all : * * * If is a set and a binary relation on , we call the pair a partial order text/html 2015-02-22T14:01:32+0200 Anonymous (anonymous@undisclosed.example.com) phantm https://lara.epfl.ch/w/phantm?rev=1424610092&do=diff Phantm : PHP Analyzer for Type Mismatch Welcome to the phantm wiki! Phantm analyzes PHP code statically (with optional help from dynamic instrumention). It has found many errors in real PHP applications. News 05.10.2012: phantm 1.0.7 has been released, see text/html 2017-08-22T16:21:37+0200 Anonymous (anonymous@undisclosed.example.com) phd_positions https://lara.epfl.ch/w/phd_positions?rev=1503411697&do=diff PhD Positions [PhD EPFL] Click Here for the Official Page Open Positions: Laboratory for Automated Reasoning and Analysis (LARA) is generally looking for outstanding students interested in pursuing a doctoral (PhD) program in the area of verification, software analysis, automated reasoning, programming languages, and software reliability. PhD students are expected to maintain active research activity, as well as attend doctoral classes and assist in teaching. text/html 2007-11-07T14:25:13+0200 Anonymous (anonymous@undisclosed.example.com) pmatching https://lara.epfl.ch/w/pmatching?rev=1194441913&do=diff Pattern matching project Yet another page... Attempt to link to another page.. SVN All sources are available from a publicly accessible SVN repository. Valuable Papers [1] T. Millstein, Practical Predicate Dispatch, OOPSLA'04, Oct. 24-28 2004 [2] M. Pettersson, A Term Pattern-Match Compiler Inspired by Finite Automata Theory text/html 2013-11-19T17:22:35+0200 Anonymous (anonymous@undisclosed.example.com) pong https://lara.epfl.ch/w/pong?rev=1384878155&do=diff Pong Designer : Game Programming by Demonstration The increasing adoption of smartphones and tablets has provided tens of millions of users with substantial resources for computation, communication and sensing. The availability of these resources has a huge potential to positively transform our society and empower individuals. Unfortunately, although the number of users has increased dramatically, the number of developers is still limited by the high barrier that existing programming environmen… text/html 2009-04-08T01:22:37+0200 Anonymous (anonymous@undisclosed.example.com) predicate_abstraction https://lara.epfl.ch/w/predicate_abstraction?rev=1239146557&do=diff Some predicate abstraction papers: * Construction of abstract state graphs with PVS * Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format) * Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213 * Bebop: a path-sensitive interprocedural dataflow engine, Thomas Ball, Sriram K. Rajamani. PASTE 2001: 97-103 … text/html 2007-03-30T20:52:40+0200 Anonymous (anonymous@undisclosed.example.com) preorder https://lara.epfl.ch/w/preorder?rev=1175280760&do=diff Preorder A (reflexive) preorder relation on set is a binary relation that is reflexive and transitive, that is, these two properties hold: * * Constructing a partial order from a preorder Intuitively, preorder differs from partial order in that there are distinct elements that have same ordering properties with respect to other elements. For such elements we therefore have text/html 2010-04-15T12:08:50+0200 Anonymous (anonymous@undisclosed.example.com) printingposters https://lara.epfl.ch/w/printingposters?rev=1271326130&do=diff Printing Posters Here are some tips and tricks to prepare and print posters with the Reprographie service (a.k.a. repro). EPFL Logos Do not use a bitmap logo (JPG, PNG, etc.) but use the official vector logo instead, available here. Use the version in CMYK colors text/html 2012-09-21T12:11:51+0200 Anonymous (anonymous@undisclosed.example.com) programming_in_scala https://lara.epfl.ch/w/programming_in_scala?rev=1348222311&do=diff Programming in Scala The main recommended reference book for Scala: * Programming in Scala, A comprehensive step-by-step guide, by Martin Odersky, Lex Spoon, and Bill Venners For more, see the Documentation section at <http://www.scala-lang.org/> text/html 2014-11-02T16:15:43+0200 Anonymous (anonymous@undisclosed.example.com) projects-old https://lara.epfl.ch/w/projects-old?rev=1414941343&do=diff Old Projects Static code analysis for real-world Scala code base Enterprises want to “manage” code quality, enforce code standards, flag dubious code (find bugs). Gist Create an extensible static analysis tool based on the Scala front-end. Expose a simple text/html 2021-10-27T11:25:16+0200 Anonymous (anonymous@undisclosed.example.com) projects https://lara.epfl.ch/w/projects?rev=1635326716&do=diff Available Student Projects in LARA - EPFL Internal Page General LARA Projects Suggestions: <https://gitlab.epfl.ch/kuncak/student-projects/> In Spring 2022 we will accept only a limited number of semester projects of students who took Computer Language Processing or Formal Verification, because Viktor Kuncak is on a sabbatical. text/html 2019-09-18T10:56:37+0200 Anonymous (anonymous@undisclosed.example.com) publications https://lara.epfl.ch/w/publications?rev=1568796997&do=diff LARA Publications Individual Publication Lists Publication lists from home pages: * Viktor Kuncak Master's Theses (Partial List) * Philippe Suter: Non-Clausal Satisfiability Modulo Theories * Regis Blanc: Verification of Imperative Programs in Scala * Remi Bonnet: Well-structured Petri Nets extensions with data * Mikaël Mayer: Complete Program Synthesis for Linear Arithmetic * Ersoy Bayramoglu: Programming with Undo * Sebastian Gfeller: Robust Dynamically Deployed Static Analy… text/html 2010-12-14T16:55:00+0200 Anonymous (anonymous@undisclosed.example.com) publications2 https://lara.epfl.ch/w/publications2?rev=1292342100&do=diff Our publications Note: you can search for LARA publications on Infoscience See also Master's theses: * Remi Bonnet: Well-structured Petri Nets extensions with data * Mikaël Mayer: Complete Program Synthesis for Linear Arithmetic * Ersoy Bayramoglu: Programming with Undo * Sebastian Gfeller: Robust Dynamically Deployed Static Analysis for Java * Mirco Dotta: State Exploration of Scala Actor Programs * Philippe Suter: Non-Clausal Satisfiability Modulo Theories * Gizil Oguz: De… text/html 2007-05-05T13:32:33+0200 Anonymous (anonymous@undisclosed.example.com) pushdown_systems https://lara.epfl.ch/w/pushdown_systems?rev=1178364753&do=diff Pushdown systems Push down automaton and context-free grammars. Summary of results. * Stefan Schwoon's thesis: Model-Checking Pushdown Systems * R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. Reps, and M. Yannakakis. Analysis of Recursive State Machines text/html 2007-06-29T22:20:15+0200 Anonymous (anonymous@undisclosed.example.com) randomized_model_finder https://lara.epfl.ch/w/randomized_model_finder?rev=1183148415&do=diff Randomized Model Finder Cédric Jeanneret and Leander Eyer This project introduces a new method using randomness to find model for first order logic formulas. This new method has been tested on a simple example and results, even far from well-known model finder tool, are encouraging. This project also presents a solver for TPTP problems based on KodKod. text/html 2014-05-16T18:38:46+0200 Anonymous (anonymous@undisclosed.example.com) rbound https://lara.epfl.ch/w/rbound?rev=1400258326&do=diff Orb: Resource Bound Inference for Functional Programs Orb is a tool for inferring symbolic resource bounds of purely functional Scala programs that use algebraic data types, recursive functions and nonlinear operations. The latest standalone version of Orb is available text/html 2011-05-24T14:29:20+0200 Anonymous (anonymous@undisclosed.example.com) reachable_pushdown_configurations_are_regular https://lara.epfl.ch/w/reachable_pushdown_configurations_are_regular?rev=1306240160&do=diff Backward reachable pushdown configurations are regular Examples: * program with procedures that ensures proper use of a global lock * Java stack inspection from security policies; accessing a local file system for logging purposes We next show that in a push down system, the pre-image of a regular set of configurations is again a regular set of configurations. Moreover, the new finite state machine for configurations can use the same set of states as the original one. This gives an algo… text/html 2010-05-28T19:29:41+0200 Anonymous (anonymous@undisclosed.example.com) regsy-examples https://lara.epfl.ch/w/regsy-examples?rev=1275067781&do=diff Regsy - Examples * Addition unfold # MONA Presburger predicates # auxiliary predicates pred xor(var0 x,y) = x&~y | ~x&y; pred at_least_two(var0 x,y,z) = x&y | x&z | y&z; # addition relation (p "+" q = r) pred plus(var2 p,q,r) = ex2 c: # carry track 0 notin c # no carry-in & all1 t: (t+1 in c <=> at_least_two(t in p, t in q, t in c)) # propagate carry & (t in r <=> xor(xor(t in p, t … text/html 2011-01-12T17:08:28+0200 Anonymous (anonymous@undisclosed.example.com) regsy https://lara.epfl.ch/w/regsy?rev=1294848508&do=diff RegSy: A Synthesizer for Regular Specifications over Unbounded Domains RegSy (Regular Synthesis) is a synthesis tool that can be used to build functions from specification written in WS1S (or, equivalently, specifications given by automata, thanks to the WS1S-automata connection). text/html 2014-09-19T12:16:34+0200 Anonymous (anonymous@undisclosed.example.com) regular_expression https://lara.epfl.ch/w/regular_expression?rev=1411121794&do=diff Regular expressions Regular expressions are expressions denoting certain languages. They are precisely those languages that can be built from the singleton languages , and for each , using operations union (), concatenation (), and iteration () on languages. text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) regular_expressions_for_automata_with_parallel_inputs https://lara.epfl.ch/w/regular_expressions_for_automata_with_parallel_inputs?rev=1429630357&do=diff Regular Expressions and Automata with Parallel Inputs Given an alphabet , we consider a larger (but still finite) alphabet for some . Keep in mind that is just one symbol; we often write it as We can consider * regular expression * automata text/html 2013-11-07T15:42:31+0200 Anonymous (anonymous@undisclosed.example.com) rosa https://lara.epfl.ch/w/rosa?rev=1383835351&do=diff Rosa: The Real Compiler Rosa is publicly available on GitHub. text/html 2016-06-03T12:46:32+0200 Anonymous (anonymous@undisclosed.example.com) sav https://lara.epfl.ch/w/sav?rev=1464950792&do=diff Synthesis, Analysis, and Verification ---------- Here you can access the archives and the latest edition of the course Synthesis, Analysis and Verification. The latest edition of the course: SAV 2017 Previous editions are: SAV 2015, SAV 2013, SAV 2012, SAV 2011, SAV 2010, SAV 2009, SAV 2008 ---------- text/html 2007-09-16T16:14:08+0200 Anonymous (anonymous@undisclosed.example.com) sav07 https://lara.epfl.ch/w/sav07?rev=1189952048&do=diff Software Analysis and Verification (March-June 2007 Class) This class is taught next in Spring 2008. Tools for automated analysis and verification of software can greately improve reliability of software that we use every day. The underlying techniques are also used for compiler optimizations and program understanding. In recent years, new algorithms and combinations of existing techniques have made such tools more effective than in the past. This course gives an overview of basic techni… text/html 2007-06-15T11:58:03+0200 Anonymous (anonymous@undisclosed.example.com) sav07_future_lectures https://lara.epfl.ch/w/sav07_future_lectures?rev=1181901483&do=diff Probabilistic techniques * Daikon invariant generator * Program verification as probabilistic inference * Inferring bugs from within Expressive type systems * Scala language * ATS * Type-Refinements.info text/html 2007-04-12T21:34:49+0200 Anonymous (anonymous@undisclosed.example.com) sav07_homework_1 https://lara.epfl.ch/w/sav07_homework_1?rev=1176406489&do=diff SAV07 Homework 1 Here is the [Homework 1 PDF] (with some corrected typos). Here are some example ocaml programs that may help you get started with using ocaml (but see also <http://caml.inria.fr/> ). Please remove the .txt extension when saving the file. * * Note that you will need to use a slightly different syntax tree compared to one in formulas.ml, because the quantifiers in your homework are bounded. text/html 2007-03-19T12:02:07+0200 Anonymous (anonymous@undisclosed.example.com) sav07_homework_1_solution https://lara.epfl.ch/w/sav07_homework_1_solution?rev=1174302127&do=diff Task 1 The property holds. Namely, suppose . Then there is a y such that and . Therefore, and . From and we have . Similarly, from and we have . Therefore, . Task 2 The property does not hold. As an example, take A={1,2}, B={p,q} and let text/html 2007-04-06T20:15:23+0200 Anonymous (anonymous@undisclosed.example.com) sav07_homework_2 https://lara.epfl.ch/w/sav07_homework_2?rev=1175883323&do=diff Homework 2 Quantifier Elimination Consider a fragment of Presburger arithmetic where atomic formulas are equalities or inequalities of the form , for arbitrary integer variables and arbitrary constants . F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F A ::= v=v | v + K ≤ v K ::= ... -2 | -1 | 0 | 1 | 2 | ... v ::= x | y | z | ... text/html 2007-04-15T17:07:20+0200 Anonymous (anonymous@undisclosed.example.com) sav07_homework_3 https://lara.epfl.ch/w/sav07_homework_3?rev=1176649640&do=diff Forward and backward propagation Let denote the result of propagating backward the error conditions, that is, the negation of postcondition. We define by for all . Here for any set of states we write for the complement of , that is, the set text/html 2007-04-24T22:27:52+0200 Anonymous (anonymous@undisclosed.example.com) sav07_homework_4 https://lara.epfl.ch/w/sav07_homework_4?rev=1177446472&do=diff Forthcoming SAV07 Homework 4 Solution. THE PARTS BELOW ARE DUE ON APRIL 19 Weakest preconditions and relations Consider a guarded command language with one variable, denoted x, and constructs assume F assert F havoc(x) c1 [] c2 c1 ; c2 Assume that F can only mention x as the only variable, which takes values from some set text/html 2007-06-16T22:12:04+0200 Anonymous (anonymous@undisclosed.example.com) sav07_homework_4_solution https://lara.epfl.ch/w/sav07_homework_4_solution?rev=1182024724&do=diff This is a sketch of the solution of SAV07 Homework 4 Part 1 Then we have . Then we have . Note that we have . Basically, and both act as a left zeros of for the relations of the form . Part 2 It is easiest to use the definition of Galois connection given by text/html 2007-06-03T12:14:01+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_1 https://lara.epfl.ch/w/sav07_lecture_1?rev=1180865641&do=diff Lecture 1 This is introductory lecture to sav07. Here are the [slides for Lecture 1]. A good background reading for this course are some parts of Gallier Logic Book although we will review some of them. Over of the material Describe here what we do in which lecture. text/html 2007-04-03T20:31:40+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_2 https://lara.epfl.ch/w/sav07_lecture_2?rev=1175625100&do=diff Lecture 2 Will soon post a clean PDF version of our notes Manually proving an example For software verification. Programs must be represented as logical formulas. These logical formulas can be used for proving invariants. This lecture explains the base theory about Propositional logic, First Order logic and Relations. text/html 2007-03-17T20:06:46+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_2_skeleton https://lara.epfl.ch/w/sav07_lecture_2_skeleton?rev=1174158406&do=diff Lecture 2 Manually proving an example Recall our example from Lecture 1, with a loop invariant: public static int sum(int a0, int n0) /*: requires "a0 > 0 & n0 > 0" ensures "result > 0" */ { int res = 0, a = a0, n = n0; while //: inv "a > 0 & res >= 0 & (n = n0 | res > 0)" (n > 0) { a = 2*a; res = res + a; n = n - 1; } return res; } text/html 2007-04-18T09:39:46+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_3 https://lara.epfl.ch/w/sav07_lecture_3?rev=1176881986&do=diff Lecture 3 Scribe: Yuanjian Summary of what we are doing in today's class: Verification condition generation: converting programs into formulas Context Recall that we can * represent programs using guarded command language, e.g. desugaring of 'if' into non-deterministic choice and assume text/html 2007-03-21T14:27:23+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_3_skeleton https://lara.epfl.ch/w/sav07_lecture_3_skeleton?rev=1174483643&do=diff Lecture 3 (Skeleton) Summary of what we are doing in today's class: Verification condition generation: converting programs into formulas Context Recall that we can * represent programs using guarded command language, e.g. desugaring of 'if' into non-deterministic choice and assume text/html 2007-03-28T18:14:33+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_4 https://lara.epfl.ch/w/sav07_lecture_4?rev=1175098473&do=diff Lecture 4 The structure of this lecture is similar to the previous one: Today, we extend the approach from last lecture (both generating and proving formulas) to support data structures such as references and arrays. We use weakest preconditions, although you could also use strongest postconditions or any other variants of the conversion from programs to formulas. text/html 2007-03-26T14:14:14+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_4_skeleton https://lara.epfl.ch/w/sav07_lecture_4_skeleton?rev=1174911254&do=diff Lecture 4 Skeleton The structure of this lecture is similar to the previous one: Today, we extend the approach from last lecture (both generating and proving formulas) to support data structures such as references and arrays. We use weakest preconditions, although you could also use strongest postconditions or any other variants of the conversion from programs to formulas. text/html 2007-04-03T23:19:17+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_5 https://lara.epfl.ch/w/sav07_lecture_5?rev=1175635157&do=diff Lecture 5 Two important techniques: * Nelson-Oppen combination method * Proof search Basic idea of Nelson-Oppen combination We mentioned decision procedures for * quantifier-free Presburger arithmetic: by small model property * quantifier-free uninterpreted function symbols: by congruence closure text/html 2007-03-28T23:02:02+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_5_skeleton https://lara.epfl.ch/w/sav07_lecture_5_skeleton?rev=1175115722&do=diff Lecture 5 Skeleton Two important techniques: * Nelson-Oppen combination method * Proof search Basic idea of Nelson-Oppen combination We mentioned decision procedures for * quantifier-free Presburger arithmetic: by small model property * quantifier-free uninterpreted function symbols: by congruence closure text/html 2007-05-28T19:40:28+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_6 https://lara.epfl.ch/w/sav07_lecture_6?rev=1180374028&do=diff Lecture 6 Resolution theorem proving Summary of Transformation to Clauses Resolution operates on sets of clauses, which is essentially a disjunctive normal form of formulas without existential quantifiers. Skolemization is the way to remove existential quantifiers at the cost of introducing new uninterpreted function symbols; skolemization preserves satisfiability. text/html 2007-04-03T23:27:03+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_6_skeleton https://lara.epfl.ch/w/sav07_lecture_6_skeleton?rev=1175635623&do=diff Lecture 6 Skeleton Resolution theorem proving Summary of Transformation to Clauses Resolution operates on sets of clauses, which is essentially a disjunctive normal form of formulas without existential quantifiers. Skolemization is the way to remove existential quantifiers at the cost of introducing new uninterpreted function symbols; skolemization preserves satisfiability. text/html 2009-04-08T01:26:47+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_7 https://lara.epfl.ch/w/sav07_lecture_7?rev=1239146807&do=diff Lecture 7: Formulas as a unifying domain for static analysis General setup Analysis domain based on formulas and main operations: * - set of all first-order formulas (or another set closed under propositional operations and quantifiers) * - subset of formulas that we use as our analysis domain, typically finite. If we used abstract interpretation framework, we would have text/html 2007-04-04T13:08:06+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_7_skeleton https://lara.epfl.ch/w/sav07_lecture_7_skeleton?rev=1175684886&do=diff Lecture 7: Formulas as a unifying domain for static analysis General setup Analysis domain based on formulas and main operations: * - set of all first-order formulas (or other set closed under propositional operations and quantifiers) * - subset of formulas that we use as our analysis domain, e.g. finite. If we used abstract interpretation framework, we would have text/html 2007-04-12T14:16:13+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_8 https://lara.epfl.ch/w/sav07_lecture_8?rev=1176380173&do=diff Lecture 8 Substitution theorem Recall the statement in the optional part of Homework 1. Review of * semantics of first-order logic * definition of capture-avoiding substitution and the set of free variables * structural induction on algebraic data types and comparison to induction on natural numbers text/html 2007-04-12T14:15:44+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_8_skeleton https://lara.epfl.ch/w/sav07_lecture_8_skeleton?rev=1176380144&do=diff Lecture 8 Skeleton Substitution theorem Recall the statement in the optional part of Homework 1. Review of * semantics of first-order logic * definition of capture-avoiding substitution and the set of free variables * structural induction on algebraic data types and comparison to induction on natural numbers text/html 2007-05-11T17:26:29+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_9 https://lara.epfl.ch/w/sav07_lecture_9?rev=1178897189&do=diff Lecture 9: Fixpoints in static analysis Recall formula propagation from Lecture 7. See correctness of formula propagation. Static analysis as equation solving in a lattice If instead of formulas as we have elements of some lattice, this condition becomes (where sp in now denotes operator on states and not formulas). text/html 2007-04-19T11:53:39+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_9_skeleton https://lara.epfl.ch/w/sav07_lecture_9_skeleton?rev=1176976419&do=diff Lecture 9 Skeleton Recall formula propagation from Lecture 7. See correctness of formula propagation. Static analysis as equation solving in a lattice If instead of formulas as we have elements of some lattice, this condition becomes (where sp in now denotes operator on states and not formulas). text/html 2007-04-24T21:40:24+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_10 https://lara.epfl.ch/w/sav07_lecture_10?rev=1177443624&do=diff Lecture 10 Guest lecture by Andrey Rybalchenko: * Andrey's web page with links to papers * Links to paper pdfs text/html 2007-04-19T11:53:27+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_10_skeleton https://lara.epfl.ch/w/sav07_lecture_10_skeleton?rev=1176976407&do=diff Lecture 10 Skeleton Guest lecture by Andrey Rybalchenko: * Andrey's web page with links to papers * Links to paper pdfs ASTREE Static Analyzer A Static Analyzer for Large Safety-Critical Software Link to paper Section 5.4: A remark on notation: * if denotes the state and is a deterministic statement, then text/html 2007-04-25T18:17:52+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_11 https://lara.epfl.ch/w/sav07_lecture_11?rev=1177517872&do=diff Lecture 11 Modular analysis of procedures Inlining specifications. Last part of SAV07 Homework 4. Postconditions that refer to values of variables in the precondition. The meaning of modifies clauses. ASTREE Static Analyzer The Octagon Abstract Domain Link to paper A Static Analyzer for Large Safety-Critical Software text/html 2007-04-25T17:44:23+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_11_skeleton https://lara.epfl.ch/w/sav07_lecture_11_skeleton?rev=1177515863&do=diff Modular analysis of procedures Inlining specifications. Last part of SAV07 Homework 4. Postconditions that refer to values of variables in the precondition. The meaning of modifies clauses. ASTREE Static Analyzer The Octagon Abstract Domain Link to paper A Static Analyzer for Large Safety-Critical Software text/html 2007-04-30T16:58:53+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_12 https://lara.epfl.ch/w/sav07_lecture_12?rev=1177945133&do=diff Constraint-based analysis * Sting tool, Constraint-based Linear-Relations Analysis Key techniques: * postulate a linear template invariant * formulate standard condition for inductive invariant over templates * eliminate implication using Farkas lemma * remove existential quantifiers using text/html 2007-04-26T13:43:50+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_12_skeleton https://lara.epfl.ch/w/sav07_lecture_12_skeleton?rev=1177587830&do=diff Constraint-based analysis * Sting tool, Constraint-based Linear-Relations Analysis Key techniques: * postulate a linear template invariant * formulate standard condition for inductive invariant over templates * eliminate implication using Farkas lemma * remove existential quantifiers using text/html 2007-05-02T15:20:50+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_13 https://lara.epfl.ch/w/sav07_lecture_13?rev=1178112050&do=diff Predicate abstraction techniques (first part) See predicate abstraction papers. Three aspects: * abstraction * model checking (finite state or pushdown system) * counterexample-driven refinement Today: abstraction Abstraction Main readings: * Construction of abstract state graphs with PVS * Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format) * Automatic Predicate Abstracti… text/html 2007-05-02T15:19:48+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_13_skeleton https://lara.epfl.ch/w/sav07_lecture_13_skeleton?rev=1178111988&do=diff Predicate abstraction techniques See predicate abstraction papers. Three aspects: * abstraction * model checking (finite state or pushdown system) * counterexample-driven refinement Today: abstraction Abstraction Main readings: * Construction of abstract state graphs with PVS * Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format) * Automatic Predicate Abstraction of C Progr… text/html 2007-05-03T19:03:22+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_14_skeleton https://lara.epfl.ch/w/sav07_lecture_14_skeleton?rev=1178211802&do=diff Predicate abstraction techniques continued See predicate abstraction papers. Recall three aspects: * abstraction * model checking (finite state or pushdown system) * counterexample-driven refinement Today we deal with the last two. Reachability checking for finite state systems using BDDs text/html 2007-05-10T11:57:55+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_15 https://lara.epfl.ch/w/sav07_lecture_15?rev=1178791075&do=diff Lecture 15 * Introduction to using MSOL over strings to verify linked lists * Strings and languages * Finite state machine * Determinization of finite state machine Automata and languages: * Introduction to the Theory of Computation * Introduction to Automata Theory, Languages, and Computation Verification of linked structures using automata or MSOL: * Field constraint analysis * Pointer Assertion Logic Engine text/html 2007-05-07T10:56:06+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_15_skeleton https://lara.epfl.ch/w/sav07_lecture_15_skeleton?rev=1178528166&do=diff Finite state machines and verification of programs that manipulate linked lists * Introduction to using MSOL over strings to verify linked lists * 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 * Using automata to decide Presburger arithmetic * MSOL … text/html 2007-05-10T18:38:37+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_16 https://lara.epfl.ch/w/sav07_lecture_16?rev=1178815117&do=diff Lecture 16 (A sequel to SAV07 Lecture 15.) * Finite state machine with epsilon transitions * Closure properties of finite state machines * Regular expression * Equivalence of finite state machine and regular expression languages * Using automata to decide Presburger arithmetic * MSOL over strings Automata and languages: * Introduction to the Theory of Computation * Introduction to Automata Theory, Languages, and Computation MSOL: * The MONA Project More * LASH Toolse… text/html 2007-05-16T00:12:25+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_17 https://lara.epfl.ch/w/sav07_lecture_17?rev=1179267145&do=diff Lecture 17 A sequel to SAV07 Lecture 16 and SAV07 Lecture 15. Preliminary reading: * Tree Automata Techniques and Applications (Tata book), pages 13-20 * <http://www.brics.dk/mona/papers/implementation-secrets/journal.pdf> Topics to cover: * Using automata to decide MSOL over finite strings * Regular expressions for automata with parallel inputs * Expressing finite automata in MSOL over strings * Expressing regular expressions in MSOL over strings * Encoding lists using MSOL … text/html 2007-06-19T21:43:20+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_18 https://lara.epfl.ch/w/sav07_lecture_18?rev=1182282200&do=diff Lecture 13: Concurrency (See also SAV07 Lecture 26.) A language with concurrency primitives c ::= [r] | c[]c | c;c | c* | c||c | atomic(c) [r] - havoc, assume, assert, assignments, any simple command, given by relation r Examples What are the possible results? text/html 2007-05-31T12:14:03+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_19 https://lara.epfl.ch/w/sav07_lecture_19?rev=1180606443&do=diff Lecture 19 (Presented by Ruzica Piskac.) Push-down automata Equivalence of push-down automata and context-free grammars. Intersection of a regular and context-free language. First-order theorem provers Completeness of propositional resolution. text/html 2009-05-27T10:28:30+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_20 https://lara.epfl.ch/w/sav07_lecture_20?rev=1243412910&do=diff Lecture 20: Interprocedural Analysis - Introduction intraprocedural analysis = analysis for language without procedures interprocedural analysis = analysis for language with procedures Given intraprocedural analysis, how do we create interprocedural analysis? text/html 2009-05-27T10:26:25+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_21 https://lara.epfl.ch/w/sav07_lecture_21?rev=1243412785&do=diff Lecture 21: More on interprocedural analysis The idea is to avoid having to specify contracts for all procedures * abstract interpretation for general case (precision depends on the example) * decidability results: no approximation, but works for restricted classes of programs (which can be obtained by abstract interpretation) text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_22 https://lara.epfl.ch/w/sav07_lecture_22?rev=1429630357&do=diff Lecture 22: Set constraints Introduction We can view analysis and verification as two stage process program + properties => system of equations/formulas => solution In general, the system of equations (for a program expressed as one loop) is an approximation of the condition text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_23 https://lara.epfl.ch/w/sav07_lecture_23?rev=1429630357&do=diff Lecture 23: Analysis of procedures, objects, and pointers Announcements: * semester and master's projects * SAV07 mini projects (Continuing sav07_lecture_22.) Analysis of object-oriented languages * Fast and Effective Optimization of Statically Typed Object-Oriented Languages (includes description of Rapid Type Analysis algorithm) Example of the problem Given the following object-oriented code : text/html 2008-05-21T11:03:00+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_24 https://lara.epfl.ch/w/sav07_lecture_24?rev=1211360580&do=diff Lecture 24: Pointer and shape analysis Always active area of research. We could say: “every analysis grows until it incorporates a pointer analysis”. Introduction Pointers and references: a way to manipulate values through a level of indirection. text/html 2007-06-21T10:22:48+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_25 https://lara.epfl.ch/w/sav07_lecture_25?rev=1182414168&do=diff Lecture 25: Presentation of relevant papers Format of this class For each project group: * pick one paper, as relevant to your project as possible * jointly present the paper in the class (if possible every group member should talk) * also give a status report on where your project is and what remains to be done text/html 2007-07-03T01:11:55+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_26 https://lara.epfl.ch/w/sav07_lecture_26?rev=1183417915&do=diff Concurrency II (See also SAV07 Lecture 18.) Concurrency aspects of Java * Ways to create (“spawn” or “fork”) threads * locks, global and per-object, relationship to atomicity Ways to create ("spawn" or "fork") threads There are two ways to create threads in Java: subclassing the Thread class or using the Runnable interface: text/html 2007-06-15T12:24:03+0200 Anonymous (anonymous@undisclosed.example.com) sav07_lecture_27 https://lara.epfl.ch/w/sav07_lecture_27?rev=1181903043&do=diff Lecture 27: Project presentations See and update SAV07 Projects page. Presentations will start promptly at 14:15. Please come a few minutes earlier to prepare. Each talk will be 15 minutes, followed by 5 minute questions and break. Times will be strictly enforced, so make sure your presentations finishes in 15 minutes. text/html 2007-06-15T12:08:10+0200 Anonymous (anonymous@undisclosed.example.com) sav07_mini_projects https://lara.epfl.ch/w/sav07_mini_projects?rev=1181902090&do=diff SAV'07 Mini projects 2 goals * do something interesting * practice communication of research results (make results look interesting and promising) Final result: * if implementation, an implemented system * in any case: write a 5-10 page paper in conference format, describing text/html 2007-05-02T16:33:59+0200 Anonymous (anonymous@undisclosed.example.com) sav07_project_ideas https://lara.epfl.ch/w/sav07_project_ideas?rev=1178116439&do=diff Project Ideas * you are not restricted to these ideas, but please discuss the suggestions with me first * some of the projects below have been assigned already * once you know which project you will like to do and you discussed it with me, email me with project title and names of people on the project text/html 2007-07-13T13:55:17+0200 Anonymous (anonymous@undisclosed.example.com) sav07_projects https://lara.epfl.ch/w/sav07_projects?rev=1184327717&do=diff SAV07 Projects Please create or update the page for your project but keep the ordering of projects. * Verifying pattern matching with guards * Randomized Model Finder * Verifying data structures using Jahob * Verifying Dijkstra's algorithm in Jahob * Expressive Power of a Fragment of WS1S * Software Verification Tools Overview * Variable range analysis * Interfaces for atomicity * Constraint based analysis of Java using Jahob and AMRC * Alloy in Jahob More information * … text/html 2007-03-20T20:57:34+0200 Anonymous (anonymous@undisclosed.example.com) sav07_quiz_answers https://lara.epfl.ch/w/sav07_quiz_answers?rev=1174420654&do=diff These are answers to selected questions. * Is the following statement valid when x is a real number and f is a function from reals to reals, and why: "If (f(x))^2 = 4, then f(x)=2" * Answer: Not valid. Let x be an arbitrary element. Take as t interpretation a function f and such that f(x)=-2. text/html 2008-04-06T13:20:55+0200 Anonymous (anonymous@undisclosed.example.com) sav07_resource https://lara.epfl.ch/w/sav07_resource?rev=1207480855&do=diff Resources on Software Analysis and Verification Related lecture notes and books * Resources for a CMU Course * CS242 from Stanford by John Mitchell * Decision procedures lectures by Jochen Hoenicke and Andreas Podelski * Proof Theory material * The KeY Approach * Decision procedures book with slides * Language proof and logic * The Calculus of Computation: Decision Procedures with Applications to Verification * Lecture notes on static analysis by Michael Schwartzbach (section… text/html 2008-02-15T16:48:30+0200 Anonymous (anonymous@undisclosed.example.com) sav08 https://lara.epfl.ch/w/sav08?rev=1203090510&do=diff Click here for Software Analysis and Verification text/html 2009-02-19T20:42:39+0200 Anonymous (anonymous@undisclosed.example.com) sav09 https://lara.epfl.ch/w/sav09?rev=1235072559&do=diff Perhaps you were looking for the SAV 09 main page? text/html 2011-02-19T23:18:05+0200 Anonymous (anonymous@undisclosed.example.com) sav11 https://lara.epfl.ch/w/sav11?rev=1298153885&do=diff Perhaps you are looking for SAV 2011? For SAV 2011, please see: <http://lara.epfl.ch/w/sav11:top> text/html 2012-02-27T12:30:28+0200 Anonymous (anonymous@undisclosed.example.com) scalaz3 https://lara.epfl.ch/w/scalaz3?rev=1330342228&do=diff Scala^Z3: Integration of Scala and Z3 Distribution The sources are now available on GitHub. Please use GitHub's issue tracker to report bugs or suggest improvements. Questions should be asked on Stack Overflow, preferably tagged with [z3] and [scala]. Paper and Presentation text/html 2011-07-22T19:38:14+0200 Anonymous (anonymous@undisclosed.example.com) scp https://lara.epfl.ch/w/scp?rev=1311356294&do=diff SCP - Constraint Programming in Scala * The sources of SCP (also known as Kaplan) bundled with Leon are available here. * You will need the Z3 and ScalaZ3 libraries to compile and run the systems. * The related Leon verification system. text/html 2013-10-20T23:40:28+0200 Anonymous (anonymous@undisclosed.example.com) semantic https://lara.epfl.ch/w/semantic?rev=1382305228&do=diff Resources and papers on semantic-enriched text [Prolog and Natural Language Analysis] Courses * EACL Links * Natural Language Processing at Stanford, by Manning * lecture16 transcript * Natural (Language) Temporal Logic: Reasoning about Absolute and Relative Time * [Automatic Inspection of Industrial Use Case Models] Resource: * <http://www.delph-in.net/erg/> Computational Semantics * [Interpretation as Abduction] * lisp seminar nlp 2008 * work by Michael Collins at… text/html 2007-05-05T16:10:36+0200 Anonymous (anonymous@undisclosed.example.com) semigroup https://lara.epfl.ch/w/semigroup?rev=1178374236&do=diff Semigroup Semigroup is a pair where such that is associative, that is, for all , text/html 2007-05-14T12:01:47+0200 Anonymous (anonymous@undisclosed.example.com) simple_linked_list_operation_in_jahob https://lara.epfl.ch/w/simple_linked_list_operation_in_jahob?rev=1179136907&do=diff Simple linked list operation in Jahob The following is an example of a method and its annotation in the Jahob verification system. class Node { public /*: claimedby List */ Node next; } class List { private static Node first; /*: public static specvar content :: objset; vardefs "content == {x. x ~= null & (first,x) : {(v,w). v..Node.next=w}^*}"; public static specvar pointed :: "obj => bool"; public vardefs "pointed == (% n. EX x. x ~= null & x..Node.next = n)… text/html 2009-01-30T12:14:15+0200 Anonymous (anonymous@undisclosed.example.com) sizedatatree.java https://lara.epfl.ch/w/sizedatatree.java?rev=1233314055&do=diff Insertion into Tree with Data and Size Fields public final class Node { public /*: claimedby Tree */ Node right; public /*: claimedby Tree */ Node left; public /*: claimedby Tree */ Object data; } public class SizeDataTree { private static Node root; private static int size; /*: private static specvar inlist :: objset; public static specvar content :: objset; private vardefs "inlist == {x. rtrancl_pt (% x y. x..Node.left = y | x..Node.right = y) root x}… text/html 2009-01-30T13:07:36+0200 Anonymous (anonymous@undisclosed.example.com) sizelist.java https://lara.epfl.ch/w/sizelist.java?rev=1233317256&do=diff Insertion and Removal from a List with Size Field class Node { public /*: claimedby SizeList */ Node next; } class SizeList { private static Node root; private static int size; /*: public static specvar content :: objset; vardefs "content == {n. n ~= null & (root,n) : {(u,v). u..next=v}^*}"; invariant sizeInv: "size = cardinality content"; invariant treeInv: "tree [next]"; invariant rootInv: "root ~= null --> (ALL n. n..next ~= root)"; invariant noNex… text/html 2013-11-19T10:06:56+0200 Anonymous (anonymous@undisclosed.example.com) slickchair https://lara.epfl.ch/w/slickchair?rev=1384852016&do=diff Slick Chair: An Open-Source Conference Management System in Scala <https://github.com/SlickChair/SlickChair> text/html 2013-12-09T10:18:24+0200 Anonymous (anonymous@undisclosed.example.com) slin https://lara.epfl.ch/w/slin?rev=1386580704&do=diff Speculative Linearizability Automata Specification in Isabelle/HOL [Archive containing the theory files] An older version of the theory can be found in the Archive of Formal Proofs. Abortable Linearizable Modules in the AFP TLA+ Specifications [TLA+ Specifications] I/O automata with finite trace semantics in Isabelle/HOL [IOA framework with finite trace semantics] text/html 2013-04-08T11:16:08+0200 Anonymous (anonymous@undisclosed.example.com) smartfloat https://lara.epfl.ch/w/smartfloat?rev=1365412568&do=diff SmartFloat: Numerical Error Estimator SmartFloat is a numerical data type library for sound floating-point computations in Scala. The library can perform sound computations with ranges of floating-point numbers and estimate the roundoff errors commited. text/html 2011-01-18T16:01:11+0200 Anonymous (anonymous@undisclosed.example.com) snisy https://lara.epfl.ch/w/snisy?rev=1295362871&do=diff Snippet Synthesis Tool SniSy is a tool for interactive snippet synthesis. text/html 2019-09-18T11:35:23+0200 Anonymous (anonymous@undisclosed.example.com) software https://lara.epfl.ch/w/software?rev=1568799323&do=diff Software The following software tools are currently available, sorted approximately according to how recently they have been updated: * Stainless - Verifier for Scala * Leon - Verifier and Synthesizer for Scala * CVC4 - CVC4 SMT Solver * Orb - Resource Bound Inference for Functional Programs text/html 2009-01-14T17:17:53+0200 Anonymous (anonymous@undisclosed.example.com) software_verification_tools_overview https://lara.epfl.ch/w/software_verification_tools_overview?rev=1231949873&do=diff Software Verification Tools Overview by Clément Beffa, Vincent Pazeller, and Olivier Gobet Report Abstract : Bugs are becoming a bigger concern nowadays as we are seeing their huge cost. Academics are building numerous tools to get rid of them with more or less success. In this paper, we make an overview of bug finding tools and focus deeper on those targeting Java code. We explain the purpose of each of them and test automatic tools on a specially built Java test case in order to see their a… text/html 2013-04-26T21:12:23+0200 Anonymous (anonymous@undisclosed.example.com) solver https://lara.epfl.ch/w/solver?rev=1367003543&do=diff Constraint Solver in Scala This is a part of GSOC in Scala: * <http://www.scala-lang.org/gsoc2013> The goal of this project is to develop a reasonably efficient constraint solver in Scala. You will build on a SAT solver we are developing and will add incremental SAT solving capabilities as well as reasoning about functional data structures. The constraint solver can be used for constraint programming, automated testing, verification, and synthesis in Scala. text/html 2009-01-30T12:24:57+0200 Anonymous (anonymous@undisclosed.example.com) sortedlist.java https://lara.epfl.ch/w/sortedlist.java?rev=1233314697&do=diff Insertion and Removal from a Sorted List class SortedList /* sorted list */ { private static Node first; /*: private static specvar reach :: "obj => obj => bool"; vardefs "reach == (% a b. rtrancl_pt (% x y. x..next=y) a b)"; public static specvar content :: objset; vardefs "content == {n. n ~= null & (first, n) : {(x,y). x..next = y}^*}"; invariant "tree [next]"; invariant "first = null | (ALL n. n..next ~= first)"; i… text/html 2023-08-28T21:31:57+0200 Anonymous (anonymous@undisclosed.example.com) start https://lara.epfl.ch/w/start?rev=1693251117&do=diff Scientific Staff See also the official list of past and current PhD students and automatically generated administrative page of the group. Support Academic Alumni Joining LARA and EPFL IC Information on joining and collaborating with LARA: * About IC * for postdoc positions, email Viktor Kuncak and check EPFL Fellows program ([PDF document]) * PhD Positions and information about EPFL * [Slides from a Seminar for Starting PhD Students] (September 2009, somewhat context-specif… text/html 2019-07-02T16:16:51+0200 Anonymous (anonymous@undisclosed.example.com) strings_and_languages https://lara.epfl.ch/w/strings_and_languages?rev=1562077011&do=diff Strings and languages We next formalize mathematically the notion of a string and a set of strings. Alphabet is a finite set of elements. (It represents characters of a string.) Let's denote it . A string is a potentially empty, finite sequence of alphabet elements. Often strings are called text/html 2014-02-11T14:37:15+0200 Anonymous (anonymous@undisclosed.example.com) stringsolver https://lara.epfl.ch/w/stringsolver?rev=1392125835&do=diff The StringSolver project is hosted on Github: StringSolver on Github Some videos for demonstration are available here: * Semi-automatic renaming on Windows * Extracting data based on file content and the three dots '...' * Grouping files to pdf using "auto" command * Semi-automatic renaming in bash (oldest video) text/html 2011-06-14T02:39:27+0200 Anonymous (anonymous@undisclosed.example.com) suri https://lara.epfl.ch/w/suri?rev=1308011967&do=diff EPFL Summer Research Institute Schedule - LARA Information Main pages: TOP, SCHEDULE Schedule Outline Monday 10:15: Applied Logic 14:15 Relational Analysis of Non-deterministic Integer Programs 15:15 Specification-Centered Robustness 16:15 Uniform Reduction to SAT and SMT Tuesday 10:15 Boolean Satisfiability: From Theoretical Hardness to Practical Success 11:15 In Praise of Algebra 14:15 Scalable Software Model Checking for Finding Bugs in the Large 15:15 HMC: Refinement type inference… text/html 2010-06-15T17:31:53+0200 Anonymous (anonymous@undisclosed.example.com) sverd https://lara.epfl.ch/w/sverd?rev=1276615913&do=diff Scala Verification Day: 15 June 2010 Location: INR 113 Meeting of the following three research groups: * LAMP, EPFL * Programming Methodology, ETHZ * LARA, EPFL with selected talks open to public. Opening talks: * 10:15 Viktor Kuncak: overview * 11:00 Peter Mueller: overview * 11:45 Martin Odersky: Interactive Q&A Session text/html 2017-03-08T09:16:35+0200 Anonymous (anonymous@undisclosed.example.com) svtp17 https://lara.epfl.ch/w/svtp17?rev=1488960995&do=diff Software Reliability and Constraint Solving Workshop Date: 8 March 2017 Location: EPFL, BC 410 Speakers: * Nikolaj Bjørner * Sergio Giro * Rustan Leino * Bruno Marnette * Philippe Rümmer 09:00. Coffee 09:30. Rustan Leino: Well-founded functions, induction, and extreme predicates in an SMT-based verifier An SMT solver takes first-order formulas as input and provides impressive automation. But what if the problem at hand goes beyond first order? The Dafny program verifier provid… text/html 2007-05-11T17:45:40+0200 Anonymous (anonymous@undisclosed.example.com) tarski_fixed_point_theorem https://lara.epfl.ch/w/tarski_fixed_point_theorem?rev=1178898340&do=diff Tarski's fixed point theorem A complete lattice is a lattice where every set of elements has the least upper bound and the greatest lower bound (this implies that there is top and bottom as and . (Note: if you know that you have least upper bounds for all sets, it follows that you also have greatest lower bounds, by taking the least upper bound of the lower bounds. Converse also holds, dually.) text/html 2020-06-23T16:19:00+0200 Anonymous (anonymous@undisclosed.example.com) teaching https://lara.epfl.ch/w/teaching?rev=1592921940&do=diff Teaching LARA is (co)responsible for the following courses: * Fall 2020: * Computer Language Processing 2020 * Formal Verification 2020 * Functional Programming 2020 * Fall 2019: * Computer Language Processing 2019 * Formal Verification 2019 * Functional Programming 2019 * Spring 2019: * Parallelism and Concurrency 2019 (internal page on courseware.epfl.ch) text/html 2016-07-14T16:54:33+0200 Anonymous (anonymous@undisclosed.example.com) test https://lara.epfl.ch/w/test?rev=1468508073&do=diff test latex: test iframe: text/html 2008-02-14T15:18:15+0200 Anonymous (anonymous@undisclosed.example.com) test_draw https://lara.epfl.ch/w/test_draw?rev=1202998695&do=diff TEST of draw plugin Plugin is : <http://wiki.splitbrain.org/plugin:draw> test02 <draw name=fabien2> text/html 2008-09-29T14:59:37+0200 Anonymous (anonymous@undisclosed.example.com) test_folded https://lara.epfl.ch/w/test_folded?rev=1222693177&do=diff This is example text with some of it only shown when you unfold it++. And after that the text just continues to flow in the same paragraph. voila voila This is example text. Title This table is only shown when you unfold the block migration text/html 2021-01-21T18:09:37+0200 Anonymous (anonymous@undisclosed.example.com) test_latex https://lara.epfl.ch/w/test_latex?rev=1611248977&do=diff Start fabien We define concatenation and iteration of languages by again End text/html 2009-01-30T12:21:27+0200 Anonymous (anonymous@undisclosed.example.com) threadedtree.java https://lara.epfl.ch/w/threadedtree.java?rev=1233314487&do=diff Insertion into a Sorted Threaded Tree public final class Node { public /*: claimedby Tree */ Node right; public /*: claimedby Tree */ Node left; public /*: claimedby Tree */ Node next; public /*: claimedby Tree */ int v; } public class ThreadedTree { private static Node root; private static Node first; /*: public static specvar content :: objset; private vardefs "content == {x. rtrancl_pt (% x y. x..left = y | x..right = y) root x}"; invariant "tre… text/html 2008-10-17T18:01:23+0200 Anonymous (anonymous@undisclosed.example.com) tips https://lara.epfl.ch/w/tips?rev=1224259283&do=diff Tips for Effective Web Editing Editing Text using a Decent Editor With this, you will be able to press a few keys and bring up your favorite editor containing the wiki page to edit, then save it back, often without even using your mouse. The description is for Linux Debian Firefox, but it should also work on some other platforms. text/html 2015-04-21T17:32:37+0200 Anonymous (anonymous@undisclosed.example.com) tree_automata https://lara.epfl.ch/w/tree_automata?rev=1429630357&do=diff Tree automata Finite Automata as Automata in Unary Language Consider a finite alphabet . A word is a finite sequence of symbols from . We can represent such a sequence as a term, as follows * treat elements of as unary function symbols * let text/html 2010-05-25T10:48:54+0200 Anonymous (anonymous@undisclosed.example.com) treeinsertion.java https://lara.epfl.ch/w/treeinsertion.java?rev=1274777334&do=diff public class Tree { private static Node root; /*: public static specvar content :: objset; private vardefs "content == {x. rtrancl_pt (% x y. x..Node.left = y | x..Node.right = y) root x}"; invariant "tree [Node.left, Node.right]"; invariant "root = null | (ALL n. n..Node.left ~= root & n..Node.right ~= root)"; invariant "ALL x y. x ~= null & y ~= null & (x..Node.right = y | x..Node.left = y) --> y : content"; invariant "ALL x y.… text/html 2014-01-10T08:32:24+0200 Anonymous (anonymous@undisclosed.example.com) useful https://lara.epfl.ch/w/useful?rev=1389339144&do=diff Some Useful Links Trello: * Leon * Trustworthy Numerics * Viktor work internal Printers * LPDLP2 (INR) * LAMPLP1 (BC) GIT * <http://lara.epfl.ch/w/laragit> LARA Phonebook * LARA phones Mailing List * <http://laraserver.epfl.ch/wws> EPFL Links * is-academia * Hotels * finances: <http://infocentre-sap.epfl.ch/> * admissions * service financier: <http://sf.epfl.ch/> * MSc courses: <http://ic.epfl.ch/page57856.html> * food: <http://restauration.epfl.ch> * … text/html 2007-05-16T10:46:42+0200 Anonymous (anonymous@undisclosed.example.com) using_automata_to_decide_msol_over_finite_strings https://lara.epfl.ch/w/using_automata_to_decide_msol_over_finite_strings?rev=1179305202&do=diff Using automata to decide MSOL over strings Compare this to Using automata to decide Presburger arithmetic. We will define such that for every and for all , for every matrix where for and , iff a11 ... a1k ---> v1 a21 ... a2k ---> v2 ... ... ... ... an1 ... ank ---> vn ^ | L(G) text/html 2015-04-21T17:26:25+0200 Anonymous (anonymous@undisclosed.example.com) using_automata_to_decide_presburger_arithmetic https://lara.epfl.ch/w/using_automata_to_decide_presburger_arithmetic?rev=1429629985&do=diff Using automata to decide Presburger arithmetic Minimalistic syntax for Presburger arithmetic is given by the following grammar: F ::= V=1 | V=V | V=V+V | F | F F | v. F V ::= v_1 | v_2 | ... Variables range over non-negative integers. Example formula: text/html 2007-06-30T03:30:19+0200 Anonymous (anonymous@undisclosed.example.com) variable_range_analysis https://lara.epfl.ch/w/variable_range_analysis?rev=1183167019&do=diff Variable Range Analysis By: Simon Blanchoud and Yuanjian Wang Zufferey Based on the paper of Patrick Cousot and Radhia Cousot * Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints Implemented in OCaml as we have in mind to get integrated into Jahob to be able to analyse real Java code. Goal Our goal is to compute the range of all variables in a piece of code as precisely as possible. These ranges could then be … text/html 2007-07-01T19:00:12+0200 Anonymous (anonymous@undisclosed.example.com) verifying_data_structures_using_jahob https://lara.epfl.ch/w/verifying_data_structures_using_jahob?rev=1183309212&do=diff Verifying data structures using Jahob by Feride Cetin and Kremena Diatchka Our goal is to verify the implementations in Java of simple data structures using Jahob. Abstract We have implemented some simple data structures in Java, provided specifications for properties they must specify, and attempted to verify that the implementation is correct with respect to these specifications using the verification tool Jahob. We have fully verified the implementations of a singly-linked list with a he… text/html 2007-07-06T19:01:42+0200 Anonymous (anonymous@undisclosed.example.com) verifying_dijkstra_s_algorithm_in_jahob https://lara.epfl.ch/w/verifying_dijkstra_s_algorithm_in_jahob?rev=1183741302&do=diff Verifying Dijkstra's algorithm in Jahob This project consist to a verification Case Study of an implementation of the Dijkstra algorithm. Here is the part of the code we will analyze: Report: [ final] Complete Dijkstra program: [ Dijkstra_Application] Slides: [ presentation] Here are the annotations for the verification of the Dijkstra Algorithm! text/html 2007-06-30T01:19:20+0200 Anonymous (anonymous@undisclosed.example.com) verifying_pattern_matching_with_guards https://lara.epfl.ch/w/verifying_pattern_matching_with_guards?rev=1183159160&do=diff Verifying pattern matching with guards Mirco Dotta, Philippe Suter Abstract from the final report: ---------- Pattern matching is a powerful construct for conditional execution, and is present in many programming languages, particularly in functional ones. The number and complexity of patterns in a matching expression often grows quickly as programs are written, and the task of checking the completeness or disjointness of such an expression becomes tedious. Compilers can assist programmers… text/html 2007-06-05T11:20:07+0200 Anonymous (anonymous@undisclosed.example.com) visibly_pushdown_languages https://lara.epfl.ch/w/visibly_pushdown_languages?rev=1181035207&do=diff Visibly pushdown languages What if a property that we wish to check is not regular? Note that checking inclusion, emptyness of intersection, and universality of context-free languages are all undecidable. So we cannot check (without approximation) whether a pushdown system satisfies a context-free property. This is unfortunate, as some properties are context-free. There is a class of languages that are between regular and context-free and that have good closure properties. These can be use… text/html 2007-07-11T18:42:25+0200 Anonymous (anonymous@undisclosed.example.com) ws1s_expressive_power_and_quantifier_elimination https://lara.epfl.ch/w/ws1s_expressive_power_and_quantifier_elimination?rev=1184172145&do=diff [Expressive Power of a Fragment of WS1S]