http://richmodels.epfl.ch/ 2012-05-17T00:38:54+02:00 http://richmodels.epfl.ch/ http://richmodels.epfl.ch/lib/images/favicon.ico text/html 2010-03-11T18:07:14+02:00 http://richmodels.epfl.ch/avm?rev=1268327234&do=diff AVM 2010 is in Lugano text/html 2010-07-13T10:20:55+02:00 http://richmodels.epfl.ch/avm2010?rev=1279009255&do=diff text/html 2011-02-09T19:38:13+02:00 http://richmodels.epfl.ch/cscomp?rev=1297276693&do=diff Counter Systems (a.k.a. Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as integers, floating-point or real numbers. Despite their apparent simplicity, counter systems can, in theory, model any real-life computer system, ranging from hardware circuits to programs. As a consequence, an important number of tools have emerged, addressing verification problems, such as reachability or termination, and deploying various tech… text/html 2010-04-09T14:47:27+02:00 http://richmodels.epfl.ch/encyclopedia?rev=1270817247&do=diff Encyclopedia Top Level Page Local Theories (Edited by Swen Jacobs) Collections (Edited by Ruzica Piskac) Transition Systems (Edited by Thomas Wies and Tomas Vojnar) As an example, please see this stub. text/html 2012-01-09T15:24:33+02:00 http://richmodels.epfl.ch/lat?rev=1326119073&do=diff Lecturer: Radu Iosif and Barbara Jobstmann Objectives: Many major hardware (Intel, IBM) and software (Microsoft) companies are now using the technique of Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The works of A. Pnueli, E. Clarke, E.A Emerson and J. Sifakis on algorithmic verification of systems using the Model Checking has been awarded the 1996… text/html 2009-09-18T12:48:56+02:00 http://richmodels.epfl.ch/lat1?rev=1253270936&do=diff 4 credits In the course, you will learn how specify and verify properties that give formal meaning to words such as 'eventually' and 'until' and how to automatically verify that systems satisfy such properties. You will learn about more general types of finite state machines: machines run continuously, such as a web server, and machines that accept not only words (strings) but also trees (tree automata). You will learn about some of the widely used results such as decision procedures for linear… text/html 2011-11-16T10:24:49+02:00 http://richmodels.epfl.ch/lopro?rev=1321435489&do=diff Doctoral course by Val Tannen Lecture notes 1 (pdf) Homework 1 (pdf) Lecture notes 2 (pdf) Lecture notes 3 (pdf) Lecture notes 4 (pdf) Homework 2 (pdf) Lecture notes 5 (revised) (pdf) Lecture notes 6 (pdf) Lecture notes 7 (pdf) Course Materials text/html 2010-10-15T16:33:19+02:00 http://richmodels.epfl.ch/lugano?rev=1287153199&do=diff Time: 18-19 October (Monday-Tuesday) 2010 CLICK HERE FOR THE PROGRAM OF THE EVENT Place: University in Lugano, collocated with FMCAD 2010 (program) [Lugano] The event is * Meeting of the COST Action IC0901 * COST Action IC0901 explores directions and techniques for making automated reasoning (including analysis and synthesis) applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system user… text/html 2012-04-01T08:41:10+02:00 http://richmodels.epfl.ch/manchester12?rev=1333262470&do=diff This meeting of the Rich Model Toolkit COST Action meeting is organized by Viktor Kuncak in collaboration with the VERIFY workshop and is collocated with IJCAR 2012 and part of the 2012 Alan Turing year celebration. The joint workshop will take place on June 30th and July 1st. text/html 2011-04-08T17:21:09+02:00 http://richmodels.epfl.ch/ntscomp?rev=1302276069&do=diff Numerical Transition Systems (a.k.a. Counter Systems, Counter Automata or Counter Machines) are simple models of computation involving infinite (or very large) data domains, such as naturals, integers, rationals or real numbers. Despite their apparent simplicity, NTS can, in theory, model any real-life computer system, ranging from hardware circuits to programs. As a consequence, an important number of tools have emerged, addressing verification problems, such as reachability or termination, and… text/html 2011-12-11T12:53:06+02:00 http://richmodels.epfl.ch/ntscomp_ntslib?rev=1323604386&do=diff Numerical Transition Systems Library The NTS-lib consists of a language specification (NTL), a parser for the language, abstract syntax tree classes, and a pretty-printer. The NTS-lib provides a common exchange format for numerical program benchmarks. text/html 2011-02-24T19:02:19+02:00 http://richmodels.epfl.ch/program.txt?rev=1298570539&do=diff Please see the [program as a pdf file]. text/html 2011-03-28T13:29:12+02:00 http://richmodels.epfl.ch/reimbursements?rev=1301311752&do=diff * You will get reimbursed for transportation, flight (+train), etc. for which you need to provide a receipt and boarding passes. * Accommodation is reimbursed using a flat rate per night, for which no receipts are needed. * Food is also covered with a flat rate per meal, two meals per day. * Registration fees are not covered. text/html 2011-05-08T12:31:43+02:00 http://richmodels.epfl.ch/report2011?rev=1304850703&do=diff Please enter any relevant information below and provide the relevant links. Thanks! Please provide this information by April 30th. Sorry for the late notice! --vkuncak 1) Publications that were written jointly Joint publications by authors from different participating institutions: text/html 2011-04-30T19:10:48+02:00 http://richmodels.epfl.ch/report2012?rev=1304183448&do=diff Please enter any relevant information below and provide the relevant links. Thanks! Please provide this information by April 30th. Sorry for the late notice! --vkuncak 1) Publications that were written jointly Joint publications by authors from different participating institutions: text/html 2010-01-29T17:43:34+02:00 http://richmodels.epfl.ch/rml?rev=1264783414&do=diff Syntax * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) * tools to provide nicer surface syntax and generate lisp syntax * we have a candidate using LR(1) parser (CUP) * an earlier version: Vepar Grammar text/html 2012-04-01T12:51:45+02:00 http://richmodels.epfl.ch/start?rev=1333277505&do=diff [COST LOGO] About the Initiative This rich model toolkit initiative explores directions and techniques for making automated reasoning (including analysis and synthesis) applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers. It includes participants from over 20 countries, over 50 research groups. The unifying idea of rich models is to explore precise mathematical and … text/html 2010-03-19T14:04:28+02:00 http://richmodels.epfl.ch/svarm-cfp.txt?rev=1269003868&do=diff Call for Abstracts: Synthesis, Verification, and Analysis of Rich Models http://richmodels.org/svarm http://www.easychair.org/conferences/?conf=svarm2010 The workshop on Synthesis, Verification, and Analysis of Rich Models (SVARM) will take place July 20-21 in Edinburgh, UK, as part of FLoC 2010. The event is affiliated with two FLoC conferences: IJCAR 2010 and CAV 2010. The event will be simultaneously a meeting for all work groups of the Rich Model Toolkit Initiative (http://richmodels.… text/html 2010-08-16T12:16:15+02:00 http://richmodels.epfl.ch/svarm?rev=1281953775&do=diff SVARM 2011 at ETAPS 2011 SVARM 2010 at FLoC 2010 text/html 2010-08-16T11:55:31+02:00 http://richmodels.epfl.ch/svarm10?rev=1281952531&do=diff SVARM Program Registration is through FLoC Registation Synthesis, Verification, and Analysis of Rich Models (SVARM) will take place July 20-21 in Edinburgh, UK as part of FLoC 2010. The event is affiliated with two FLoC conferences: * IJCAR 2010 * CAV 2010 text/html 2011-04-12T18:01:21+02:00 http://richmodels.epfl.ch/svarm11?rev=1302624081&do=diff SVARM Program and slides Synthesis, Verification, and Analysis of Rich Models (SVARM 2011) will take place April 1-3, 2011, as part of ETAPS 2011. Invited speakers: * Thomas A. Henzinger: Quantitative Reactive Models, Friday, April 1st, 2pm * George Candea: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems, Saturday, April 2nd, 2pm * Darko Marinov: Systematic Software Testing Using Test Abstractions, Sunday, April 3rd, 9am text/html 2011-02-09T14:59:11+02:00 http://richmodels.epfl.ch/svcomp?rev=1297259951&do=diff text/html 2011-12-21T14:04:37+02:00 http://richmodels.epfl.ch/synthesis?rev=1324472677&do=diff Topics of Interest: New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis. Working Group 4 explores the theory, tools, and usability of synthesis in system development. In contrast to automated verification algorithms, which establish whether a given system satisfies a given specification, synthesis algorithms automatically construct implementation that is guaranteed to s… text/html 2012-03-14T23:57:21+02:00 http://richmodels.epfl.ch/tallinn12?rev=1331765841&do=diff Meeting of the Rich Model Toolkit COST Action IC0901, is organized in Tallinn, Estonia, right after ETAPS 2012, in coordination with the AIPA workshop. This is a two day meeting organized in coordination with AIPA where the first day 31st of March 2012 is mainly focusing on the Automation in Proof Assistants topics, while the second day is more focused also on the other IC0901 topics, including additional invited talks, contributed talks from IC0901 Action participants, and informal technical … text/html 2010-03-11T11:35:51+02:00 http://richmodels.epfl.ch/test?rev=1268303751&do=diff Test latex: USER MAIL But also . Test VAr plugin: DATE USER Test bureaucracy: Test bureaucraty: text/html 2010-01-12T12:53:39+02:00 http://richmodels.epfl.ch/vepar_grammar?rev=1263297219&do=diff package guru.hol.parsers.isabelle; import java_cup.runtime.*; import guru.hol.ast.*; import java.util.*; parser code {: public void syntax_error(Symbol current) { IsabelleParserHelper.getReporter().error("Syntax error", current.left, current.right); } public void unrecovered_syntax_error(Symbol current) { IsabelleParserHelper.getReporter().fatalError("Couldn't repair from parsing errors"); } :}; /* Preliminaries to set up and use the JFlex scanner. */ init wit… text/html 2012-01-02T19:50:15+02:00 http://richmodels.epfl.ch/wikiname?rev=1325530215&do=diff quebec cottages manitoba cottages british columbia cottages