Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
start [2012/07/10 09:52] bingzi |
start [2013/08/01 11:41] cesar.sanchez |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| ====== Rich-Model Toolkit ====== | ====== Rich-Model Toolkit ====== | ||
| - | mulberry spring 2011 FWA | + | ===== About the Initiative ===== |
| - | compra cialis in anonimato dAlme. cialis per giovani Villafrati. comprare cialis napoli has Villanterio. It had beenswitched outIt had becomeIt was subsequentlyT have beenIt had been subsequentlyIt had been really 1977, 3 yearsseveral weeksMany years4 yearsA few yearsCouple of yearsA couple of yearsFew years After Nixon resigned HAD Underneath the Watergate scandal of cloud, the umbrella term for anyfor yourfor just oneto possess a Selection of Abuses of energy and final ,[[http://www.mulberryoutletes.com/shoulder-bags-c-1.html|Shoulder Bags]], crime Which hasThat containsThat'sThat hasThat hasGettingThat has never apologized, even. Leader, insecure, sweaty, conniving, oddly elegant. Marketers Who consume. | + | 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 formal models of key aspects of our infrastructure, developing algorithms, tools, and common standardized formats. Through our networking activities we aim to establish connections between different tools, methodologies, and communities. | ||
| - | Once theThe moment theIf theFollowing theWhenever the summer timesummer seasonthe summer seasonthe summer time several weekssummer ,[[http://www.genuinemulberryoutlet.com/|Mulberry Outlet]], time several weeksour summer timesummer time several weeks later onaheadin to the futureto come backto returnto the futurecomingto reach year finish offers Indicates ThatImplies thatImplies thatSuggests thatShows thatImplies that Will more schools Does itWill itCould itShould itWouldn't itUltimatelyHandles to get it doneMade it happen reopen? ersus chance toopportunity topossible ways topossibility toprobability topossibility foran chance topossible chance tochance returnrestore again visitinggoing tocoming atlikely tocoming tovisitinggoing to forcoming forgoing to college. Seeing normal You need to to Become to bebecomebecomebecomefinish upbecomefinish up beingswitched to be pondering: various extra supplies to possesspossessingto getto obtainyou are able to own Before heading tocoming back tohere we are atinhere i am atintodirectly intosupport in college. Including TheRelevant towards theIn regards to theConcerning theBetweenAmong theIn theInside theOne of the Whole School group of add-ons, totes Are reallyHappen to beAreHappen to beAppear to have beenWereAre usuallyAppear to become Most likely probably the mostNearly probably the mostProbably the mostBasically probably the mostThe only mostOne of the mostUndoubtedly probably the mostAmong the Key components. | + | Selected Topics of Interest: |
| + | * **Standardization of expressive languages.** Formats to represent systems, formulas, proofs, counterexamples. Translation between specification languages. Benchmarks and competitions for automated reasoning, verification, analysis, synthesis. | ||
| + | * **Decision procedures.** Decision procedures for new classes of constraints. SAT and SMT implementation and certification. Encoding synthesis and analysis problems into SMT. Description logics and scalable reasoning about knowledge bases. | ||
| + | * **Transition system analysis.** Abstraction-based approaches and refinement for verification of infinite-state systems. Constraint-based program analysis. Data-flow analysis for complex domains. Extracting transition systems from programming languages and bytecodes. | ||
| + | * **[[synthesis|High-level synthesis.]]** New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis. | ||
| - | acquisto cialis internet Cuneo. 20mg cialis Custonaci. cialis soft tabs 20mg Delebio. Out of thisDue to thisWith this particularProduced by thisFrom thatConsequentlyCreated by background in Antique THROUGHOUT Fact visit! Purpose ,[[http://www.genuinemulberryoutlet.com/|Mulberry Handbags]], far tooexcessivelyveryveryway too, baby wolves are connected withlinked toassociated withrelated toassociated withtriggered byhyperlinked torecognized to cause severala number ofa great dealnumerous Normally Explanations of. Towards the, as well asin addition tonot failing to remembernot to mentionadditionally totogether withincludingas well asplus onlybasically abasicallymerely aonly aexclusively 15-minute distressing simple method Treatment attention and care. Business-Legalities, Marketing and advertising, advertising and marketingmarketingmarketing strategiesadvertisingmarketing methodsonline marketingpromotioninternet marketing, getting yourobtaining thetaking youracquiring yourhelping yourreceving yourdelivering yourpurchasing your rehearse For manycouple ofFor severalFor manyFor a number ofFor many peopleFor manyFor individuals Decades ALSO, the reemergence tribe with tattoo designs aren'tgenerally aren't to saypublishjust one articletoto call Usually light add-ons company named moli. | + | The chair and the grant holder of the action is [[http://software.imdea.org/~cesar/|Cesar Sanchez]]. |
| - | Zeg hem dat deze zijn twee tiffany lampenschurken me you slaan zwart in blauw. '' Ik heb nog niet Klaar you wrijven Zelf nog, 'zei boer. Within theThroughout theUsing theAround the twee schurken gehouden op het als ze verslaan zong: 'Greedy pack! Diefachtige pack! Een - twee - you Geven terug zijn p boer zak! Tiffany Een rotterdam - twee - 'Dan vrouw haar tweede dochter stuurde in zei:'. | + | The Action holds general meetings typically twice a year, with one of these meetings publicized as the **SVARM** workshop. |
| - | + | ||
| - | Linke absolutely courageous Is the fact thatfrequentlyIs generally thatIs commonly thatUsually type ofkind ofkind oftype oftype ofkinds ofnumber ofparticulartypes of person, this goal is withinbecause ofis occuroccurcan there be to bold Should aussi 'reasonable bounds, one ten-year-old child When first meeting the following thethe moment thefollowingwhen theimmediately after thefollowing on in theonce the angel If you feel Is notJust is notIs simply notWon't beSeriously is notIsn'tJust isn'tIs not really feel fear? Mulberry Outlet Store [/ # 800080 size = 3 face = Calibri] If she not scared since i might be thewould be themay be thewill be theis certainly theis really asticks out because theis definitely the soi its gods, both, not scared Because Saiban Saiban Both nerve is reallyis completelyis essentiallyis extremelyis reallyis actuallyis certainlyis unquestionably largetoo big bar, drank Linke fear is perfect formight be foris really forwell suited for the sake of the productsfrom theitemsusing the productsusing thewithin thein theof the things that? This time aroundThis time around aroundNowAt this junctureThese occasionsThis occassionThis eraThis timeThat point Awen All of a sudden struck Linda madam. Linke, What isreallyPrecisely what isWhat'sParticularly what'sWhat exactly is identity? Mulberry Outlet [/ # 800080 size = 3 face = Calibri] In Awen thinking, Linke eyes suddenly progressively Get to be theFinish up being the hemoglobin, severe breathing historic ups like animal! oz saw the angel today, don't knowno cluedo not knowhave no clue ofdon't knoware not aware ofhave no ideaare unsure why goal, I trulyI have to admit iI reallyI absolutelyII honestlyMake hate you. Wish, wish all of youeverybodyeveryoneeveryoneeveryone workworkresult in the grade up! Begin, Linke is suddenly! Throughout time ofThroughoutBeforeWithin the timeThroughoutAlthoughWhenAt this time around although Linke WAS billed like a whirlpool MOST int an individualanybodyanyonepeopleonea guy or lady near tocloseness tothroughoutaroundaboutroughly historic angel, the angel and suddenly dare not play with HIM unarmed, one step backward finish occasions, although italthough itbecause itdespite the fact that iteven while italthough itwhenalthough has nothasn'thas not evernever APPEAR Our planetExistence history from holy badge and Linke ft Performed Out, and also thetogether with theas well as thein addition tofurthermore, theas well asand so the chop made aussi Initially Action Immediately Linke preventably cannot move. | + | |
| ===== Recent Activities ===== | ===== Recent Activities ===== | ||
| * Verification Modulo Theories (more information available soon) | * Verification Modulo Theories (more information available soon) | ||
| - | * [[ntscomp|(Numerical) Transition System Competition]] | + | * [[http://nts.imag.fr/index.php/Main_Page | Numerical Transition Systems]] |
| ===== Meetings ===== | ===== Meetings ===== | ||
| Line 28: | Line 31: | ||
| * **[[SVARM10|SVARM 2010]]** in Edinburgh, at [[http://www.floc-conference.org/|FLOC 2010]], July 20-21 (organization: **Paul Jackson**) | * **[[SVARM10|SVARM 2010]]** in Edinburgh, at [[http://www.floc-conference.org/|FLOC 2010]], July 20-21 (organization: **Paul Jackson**) | ||
| * **[[Lugano|Lugano 2010]]**, October 18-19, with [[http://fmcad10.iaik.tugraz.at/|FMCAD 2010]] and AVM (organization: **Viktor Kuncak** and **Natasha Sharygina**) | * **[[Lugano|Lugano 2010]]**, October 18-19, with [[http://fmcad10.iaik.tugraz.at/|FMCAD 2010]] and AVM (organization: **Viktor Kuncak** and **Natasha Sharygina**) | ||
| - | * **[[svarm11|SVARM 2011]]** meeting, 1-3 April 2011, Saarbruecken, with [[http://www.etaps.org/|ETAPS]] (organization: **Rupak Majumdar** and **Bernd Finkbeiner**) [[https://picasaweb.google.com/barbara.jobstmann/SVARM?authuser=0&authkey=Gv1sRgCNqsmMmuhZubjAE&feat=directlink|Pictures]] [[https://picasaweb.google.com/barbara.jobstmann/ETAPS?authuser=0&authkey=Gv1sRgCNjWlPfGhti-zwE&feat=directlink|Pictures of social event]] | + | * **[[svarm11|SVARM 2011]]** meeting, 1-3 April 2011, Saarbruecken, with [[http://www.etaps.org/|ETAPS]] (organization: **Bernd Finkbeiner** and **Rupak Majumdar**) [[https://picasaweb.google.com/barbara.jobstmann/SVARM?authuser=0&authkey=Gv1sRgCNqsmMmuhZubjAE&feat=directlink|Pictures]] [[https://picasaweb.google.com/barbara.jobstmann/ETAPS?authuser=0&authkey=Gv1sRgCNjWlPfGhti-zwE&feat=directlink|Pictures of social event]] |
| * [[http://www.cs.berkeley.edu/~bodik/dagstuhl-2011.html|Summer School on Synthesis]] ([[http://www.dagstuhl.de/en/program/calendar/evhp/?semnr=11322|Dagstuhl page]]), 07-12 August 2011, Dagstuhl Schloss, Germany | * [[http://www.cs.berkeley.edu/~bodik/dagstuhl-2011.html|Summer School on Synthesis]] ([[http://www.dagstuhl.de/en/program/calendar/evhp/?semnr=11322|Dagstuhl page]]), 07-12 August 2011, Dagstuhl Schloss, Germany | ||
| * **[[https://sites.google.com/site/torino2011ic0901/|Turin 2011]]** meeting, Oct 3-4, 2011, Turin, co-located with [[http://foveoos2011.cost-ic0701.org/|International Conference on Formal Verification of Object-Oriented Software]] and [[http://fmco.liacs.nl/|International Symposia on Formal Methods for Components and Objects]] (organization: **Alessandro Armando**, **Maria Paola Bonacina**, and **Luca Paolini**) [[https://picasaweb.google.com/barbara.jobstmann/20111003_Torino?authuser=0&authkey=Gv1sRgCOupzY2Mua3AVA&feat=directlink|Pictures]] | * **[[https://sites.google.com/site/torino2011ic0901/|Turin 2011]]** meeting, Oct 3-4, 2011, Turin, co-located with [[http://foveoos2011.cost-ic0701.org/|International Conference on Formal Verification of Object-Oriented Software]] and [[http://fmco.liacs.nl/|International Symposia on Formal Methods for Components and Objects]] (organization: **Alessandro Armando**, **Maria Paola Bonacina**, and **Luca Paolini**) [[https://picasaweb.google.com/barbara.jobstmann/20111003_Torino?authuser=0&authkey=Gv1sRgCOupzY2Mua3AVA&feat=directlink|Pictures]] | ||
| * **[[Tallinn12|Tallinn 2012]]** meeting collocated with **[[http://www.etaps.org/|ETAPS]] 2012** and organized by **[[http://users.ics.tkk.fi/kepa/|Keijo Heljanko]]** and **[[http://yquem.inria.fr/~herbelin/|Hugo Herbelin]]** | * **[[Tallinn12|Tallinn 2012]]** meeting collocated with **[[http://www.etaps.org/|ETAPS]] 2012** and organized by **[[http://users.ics.tkk.fi/kepa/|Keijo Heljanko]]** and **[[http://yquem.inria.fr/~herbelin/|Hugo Herbelin]]** | ||
| - | * **[[Manchester12|Manchester 2012]]** meeting organized by Viktor Kuncak in collaboration with the VERIFY workshop, collocated with [[http://ijcar.cs.manchester.ac.uk/|IJCAR 2012]] and part of the [[http://www.mathcomp.leeds.ac.uk/turing2012/|2012 Alan Turing year]] celebration | + | * **[[Manchester12|Manchester 2012]]** in collaboration with the VERIFY workshop, collocated with [[http://ijcar.cs.manchester.ac.uk/|IJCAR 2012]] and part of the [[http://www.mathcomp.leeds.ac.uk/turing2012/|2012 Alan Turing year]] celebration |
| + | * **[[Haifa12|Haifa 2012]]** meeting organized by **Eran Yahav** and **Armin Biere** | ||
| + | * **[[Rome13|Rome 2013]]** meeting organized by **Maria Paola Bonacina** and **Cesar Sanchez** | ||
| + | * **[[Malta13|Malta 2013]]** meeting organized by **Gordon Pace** and **Cesar Sanchez** | ||
| + | * {{:new.png?60|new}} **[[Madrid13|Madrid 2013]]** October, 17-18, 2013. Final meeting. | ||
| ===== Related Competitions ===== | ===== Related Competitions ===== | ||
| Line 40: | Line 47: | ||
| * [[http://www.termination-portal.org/wiki/Termination_Competition|Termination Competition]] - Proving Termination of Programs and Rewrite Systems | * [[http://www.termination-portal.org/wiki/Termination_Competition|Termination Competition]] - Proving Termination of Programs and Rewrite Systems | ||
| * [[http://fmv.jku.at/hwmcc10/|HWMCC]] - Hardware Model Checking Competition | * [[http://fmv.jku.at/hwmcc10/|HWMCC]] - Hardware Model Checking Competition | ||
| - | * [[ntscomp|NTS-COMP]] - Numerical Transition Systems Competition | + | * [[http://nts.imag.fr/index.php/Main_Page|NTS-COMP]] - Numerical Transition Systems Competition |
| Other competitions: | Other competitions: | ||
| Line 72: | Line 79: | ||
| * Mr Ronald Toegl | * Mr Ronald Toegl | ||
| * Mr Markus Rabe | * Mr Markus Rabe | ||
| - | * Dr Swen Jacobs | + | * Dr Corneliu Popeea |
| + | * Mr Simone Fulvio Rollini | ||
| + | * Dr Michael Tautschnig | ||
| + | * Mr Michał Skrzypczak | ||
| + | * Mr Hossein Hojjat | ||
| + | |||
| + | Short-Term Scientific Missions in 2013: | ||
| + | |||
| + | * Dr Ondrej Sery | ||
| + | * Mr Pavel Jancik | ||
| + | * Ondrej Lengal | ||
| + | * Andrijana Stamenkovic | ||
| [[:internal:stsm-guide|Guide to Application Process for IC0901 Members]] | [[:internal:stsm-guide|Guide to Application Process for IC0901 Members]] | ||
| Line 139: | Line 157: | ||
| * [[http://www.chalmers.se/cse/EN/people/claessen-koen|Koen Claessen]] (Sweden) | * [[http://www.chalmers.se/cse/EN/people/claessen-koen|Koen Claessen]] (Sweden) | ||
| * [[http://www.kroening.com/|Daniel Kröning]] (UK) | * [[http://www.kroening.com/|Daniel Kröning]] (UK) | ||
| - | * [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]] (Switzerland) - **Chair** | + | * [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]] (Switzerland) |
| * [[http://www.cs.utt.ro/~marius/|Marius Minea]] (Romania) | * [[http://www.cs.utt.ro/~marius/|Marius Minea]] (Romania) | ||
| * [[http://www.tcs.hut.fi/~ini/|Ilkka Niemelä]] (Finland) | * [[http://www.tcs.hut.fi/~ini/|Ilkka Niemelä]] (Finland) | ||
| Line 155: | Line 173: | ||
| * [[http://www.philipp.ruemmer.org/|Philipp Ruemmer]] (Sweden) | * [[http://www.philipp.ruemmer.org/|Philipp Ruemmer]] (Sweden) | ||
| * [[http://www.mpi-sws.mpg.de/~rybal/|Andrey Rybalchenko]] (Germany) | * [[http://www.mpi-sws.mpg.de/~rybal/|Andrey Rybalchenko]] (Germany) | ||
| - | * [[http://theory.stanford.edu/~cesar|Cesar Sanchez]] (Spain) - **Grant Holder**, MC Member | + | * [[http://theory.stanford.edu/~cesar|Cesar Sanchez]] (Spain) - **Chair and Grant Holder** |
| * [[http://www.csl.sri.com/users/shankar/|Natarajan Shankar]] (US) | * [[http://www.csl.sri.com/users/shankar/|Natarajan Shankar]] (US) | ||
| * [[http://www.imada.sdu.dk/~petersk/|Peter Schneider-Kamp]] (Denmark) [[http://ditwww.epfl.ch/cgi-perl/EPFLTV/home.pl/?page=video&lang=2&connected=0&id=650&plugin=9&checkplugin=1|Talk Video]] | * [[http://www.imada.sdu.dk/~petersk/|Peter Schneider-Kamp]] (Denmark) [[http://ditwww.epfl.ch/cgi-perl/EPFLTV/home.pl/?page=video&lang=2&connected=0&id=650&plugin=9&checkplugin=1|Talk Video]] | ||
| Line 169: | Line 187: | ||
| * [[http://www.fit.vutbr.cz/~vojnar/|Tomas Vojnar]] (Czech Republic) | * [[http://www.fit.vutbr.cz/~vojnar/|Tomas Vojnar]] (Czech Republic) | ||
| * [[http://www.cs.technion.ac.il/people/yahave/|Eran Yahav]], Technion, Israel | * [[http://www.cs.technion.ac.il/people/yahave/|Eran Yahav]], Technion, Israel | ||
| - | |||