When targeting modern parallel hardware ar chitectures\, constructing correct and highperforming software is complex and timeconsuming. In particular\, reorderings of memory accesses that vio late intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to repair these should be done sparing ly\, as they negatively impact performance.
In this work\, we propose a technique that combines model checking and static analysis to analyse sp ecifications of multithreaded software. For a given weak memory architectu re\, it identifies a set of fences to be placed in the corresponding code p roduced by our code generator. This set guarantees that the resulting softw are will be sequentially consistent. In cases where fences are not sufficie nt\, our technique suggests where to use stronger mechanisms\, such as lock ing or the use of transactional memory. In comparison\, static analysis tec hniques are less precise\, and model checking techniques have worse scalabi lity.
This is joint work with Sander de Putter.
CATEGORIES:Colloquium LOCATION:MetaForum 3.141 GEO:51.447567;5.487443 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/antonwijscheckyourloc ksandfencesintegratingmodelcheckingintofenceandtransactioninserti onanalysis/ END:VEVENT BEGIN:VEVENT UID:20190605T1405Z1559743559.3721EO5681@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190605T134701Z LASTMODIFIED:20190605T134701Z DTSTART;TZID=Europe/Amsterdam:20190606T124500 DTEND;TZID=Europe/Amsterdam:20190606T133000 SUMMARY: Jan Friso Groote: An O(m log n) algorithm for branching bisimulati on DESCRIPTION: The O(m log n) algorithm for branching bisimulation devised by Groote/Jansen/Keiren/Wijs was primarily directed towards Kripke structures and not to labelled transition systems. To verify branching bisimulation f or LTSs an explicit translation is made to Kripke structures. This ...conti nue reading XALTDESC;FMTTYPE=text/html:The O(m log n) algorithm for branching bis imulation devised by Groote/Jansen/Keiren/Wijs was primarily directed towar ds Kripke structures and not to labelled transition systems. To verify bran ching bisimulation for LTSs an explicit translation is made to Kripke struc tures. This means that the complexity for LTSs actually is O(m (log n + log Act)) and in practice the memory requirements are very high (but still O (m+n)). Together with David Jansen a dedicated algorithm has been construct ed which only requires O(m log n) and practically the current algorithm als o outperforms existing algorithms especially in memory requirements.
This is very much work in progress.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janfrisogrooteanomlo gnalgorithmforbranchingbisimulation/ END:VEVENT BEGIN:VEVENT UID:20190522T1234Z1558528459.4829EO5641@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190522T105847Z LASTMODIFIED:20190522T105847Z DTSTART;TZID=Europe/Amsterdam:20190523T124500 DTEND;TZID=Europe/Amsterdam:20190523T133000 SUMMARY: Hans Zantema: Symbolic model checking and bounded model checking DESCRIPTION: We discuss how to solve reachability problems either in BDD ba sed symbolic model checking (by NuXMV) or by bounded model checking using S MT solving. We provide several examples\, mainly from the practical assignm ents of the course ...continue reading XALTDESC;FMTTYPE=text/html:In this talk I will discuss the tangle lea rning algorithm for parity games. That is\, I will explain the concept of a tangle\, explain their role in different parity game algorithms\, and demo nstrate how we can find tangles in parity games. Furthermore I will introdu ce distractions\, simple distractions and devious distractions\, and the ro le they seem to play in parity games and how different algorithms deal with these distractions.
CATEGORIES:Colloquium LOCATION:MF 3.144 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/tomvandijkdistractions andtanglesinparitygames/ END:VEVENT BEGIN:VEVENT UID:20190508T1215Z1557317728.6934EO5491@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190508T120407Z LASTMODIFIED:20190508T120407Z DTSTART;TZID=Europe/Amsterdam:20190509T124500 DTEND;TZID=Europe/Amsterdam:20190509T133000 SUMMARY: Ferry Timmers: A complete axiomatisation for probabilistic trace e quivalence DESCRIPTION: Probabilistic labelled transition systems combine the expressi veness of Markov chains and processes. We are interested in finding a suita ble trace equivalence for such systems\, which becomes nontrival once non determinism is introduced. For this search I ...continue reading XALTDESC;FMTTYPE=text/html:Probabilistic labelled transition systems combine the expressiveness of Markov chains and processes. We are intereste d in finding a suitable trace equivalence for such systems\, which becomes nontrival once nondeterminism is introduced. For this search I have axiom atised one of the equivalences\, based on weighed traces\, which is a compl ete axiomatisation\, to gain a better understanding of its properties.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ferrytimmersacomplete axiomatisationforprobabilistictraceequivalence2/ END:VEVENT BEGIN:VEVENT UID:20190501T1447Z1556722040.8849EO5471@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190501T135037Z LASTMODIFIED:20190501T135037Z DTSTART;TZID=Europe/Amsterdam:20190502T124500 DTEND;TZID=Europe/Amsterdam:20190502T133000 SUMMARY: Jeroen Keiren: Tableaux for mucalculus model checking of infinite state systems: a note on soundness DESCRIPTION: In 1992\, Bradfield and Stirling presented a tableauxbased ap proach to local model checking of infinitestate systems that is sound and complete. When trying to apply this approach to modelchecking timed and hy brid automata against mucalculus ...continue reading XALTDESC;FMTTYPE=text/html:In 1992\, Bradfield and Stirling presented a tableauxbased approach to local model checking of infinitestate system s that is sound and complete. When trying to apply this approach to modelc hecking timed and hybrid automata against mucalculus properties we observe d that the approach is not practical. In this talk I will explain Bradfield and Stirling’s proof system\, and illustrate its limitations. I will then show how\, at the cost of losing completeness\, the proof system can be mad e more practical. Unfortunately\, the modifications break the existing soun dness proof. I therefore propose an alternative approach to the soundness p roof that is more robust when varying with the proof rules and termination conditions.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/jeroenkeirentableauxfo rmucalculusmodelcheckingofinfinitestatesystemsanoteonsoundness/ END:VEVENT BEGIN:VEVENT UID:20190423T1129Z1556018944.2851EO5451@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190423T111553Z LASTMODIFIED:20190423T111553Z DTSTART;TZID=Europe/Amsterdam:20190425T124500 DTEND;TZID=Europe/Amsterdam:20190425T133000 SUMMARY: Allan van Hulst: The quest for the mythical 57regular Moore graph DESCRIPTION: Since 1966 it is known that only four regular undirected graph s having diameter 2 and girth 5 can exist. The construction of three of the se 5\,2Moore graphs is known but it is still an open ...continue reading XALTDESC;FMTTYPE=text/html:Since 1966 it is known that only four regu lar undirected graphs having diameter 2 and girth 5 can exist. The construc tion of three of these 5\,2Moore graphs is known but it is still an open p roblem whether the remaining candidate srg(3250\,57\,0\,1) exists at all. I have developed an algorithm that constructs a partial solution to this pro blem. In particular\, I was able to remove all 3cycles and 2 of the 3 type s of 4cycles from an initial 57regular graph of order 3250. During this t alk\, I would like to tap into possible algorithmic insights of members of the group to try and see whether anyone has any ideas concerning removal of the remaining 4cycles. I will also discuss a number of earlier findings i n previous research. Notably\, and contrary to the other 5\,2Moore graphs\ , this graph cannot be vertextransitive and the order of its automorphism group is quite small (at most 375).
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/allanvanhulstthequest forthemythical57regularmooregraph/ END:VEVENT BEGIN:VEVENT UID:20190416T1333Z1555421608.1679EO5421@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190416T132821Z LASTMODIFIED:20190416T132821Z DTSTART;TZID=Europe/Amsterdam:20190418T124500 DTEND;TZID=Europe/Amsterdam:20190418T133000 SUMMARY: Rodin Aarssen: Concrete Syntax with Black Box Parsers DESCRIPTION: Meta programming is the art of writing software that takes sou rce code as input for manipulation\, analysis or code generation. Many meta programming systems reason about abstract syntax trees representing this s ource code\, which requires intimate knowledge of ...continue reading XALTDESC;FMTTYPE=text/html:Meta programming is the art of writing sof tware that takes source code as input for manipulation\, analysis or code g eneration. Many meta programming systems reason about abstract syntax trees representing this source code\, which requires intimate knowledge of the d ata type that describes the abstract syntax. Concrete syntax patterns allow meta programmers to create and perform matching on syntax trees using the actual concrete syntax of the object language. However\, meta programming s ystems that support these concrete syntax patterns generally require a conc rete grammar of the object language\, written in their own formalism. Writi ng such a grammar is a daunting\, errorprone task\, especially for nontri vial programming languages\, such as C++ and Java.
We present Concret ely\, a technique to augment meta programming systems with pluggable concre te syntax\, reusing external\, black box parsers. Concretely allows the met a programmer to use concrete syntax patterns in absence of a concrete gramm ar. Additionally\, we present Tympanic\, a DSL to declaratively map externa l parsers' AST structures to the internal data structures of the Rascal met a programming language. Algebraic data types (ADTs) for the abstract gramma r and marshalling code\, mapping the external parser's AST to the generated Rascal ADT\, are automatically generated from a Tympanic specification. Ty mpanic allows implementors of Concretely to solve the impedance mismatch pr oblem between Rascal's algebraic data types and objectoriented class hiera rchies in Java representing a grammar.
We show that for realistic pro gramming languages\, such as C++ and Java\, the effort of adding support fo r concrete syntax patterns with Concretely is in the order of dozens of sou rce lines of code (SLOC). Similarly\, we show that using Tympanic for gramm ar mapping yields a significant reduction in terms of SLOC\, compared to ma nually implementing the AST data types and marshalling code.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rodinaarssenconcretesy ntaxwithblackboxparsers/ END:VEVENT BEGIN:VEVENT UID:20190408T1105Z1554721542.9025EO5361@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190408T090245Z LASTMODIFIED:20190408T090245Z DTSTART;TZID=Europe/Amsterdam:20190411T124500 DTEND;TZID=Europe/Amsterdam:20190411T133000 SUMMARY: Wieger Wesselink: About the Design and Implementation of State Spa ce Exploration in the mCRL2 toolset DESCRIPTION: An important use case of the mCRL2 tool set is state space exp loration. An efficient and featurerich implementation is available that wo rks quite well in practice. Unfortunately the design of this implementation is quite complicated\, ...continue reading XALTDESC;FMTTYPE=text/html:An important use case of the mCRL2 tool se t is state space exploration. An efficient and featurerich implementation is available that works quite well in practice. Unfortunately the design of this implementation is quite complicated\, and there is insufficient docum entation. This makes it very hard to make any changes\, or to add new funct ionality. During the last couple of months I have implemented a completely new version of state space exploration. In this talk I will explain its des ign and implementation. The new design contains pseudo code descriptions of the underlying algorithms. I consider it very important to have pseudo cod e descriptions at the right level of abstraction\, and an implementation th at closely matches the pseudo code. Another aspect that I will discuss is h ow to keep the code for all different features separate.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/wiegerwesselinkaboutth edesignandimplementationofstatespaceexplorationinthemcrl2toolset / END:VEVENT BEGIN:VEVENT UID:20190402T1121Z1554204098.5243EO5341@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190402T111006Z LASTMODIFIED:20190402T111006Z DTSTART;TZID=Europe/Amsterdam:20190404T124500 DTEND;TZID=Europe/Amsterdam:20190404T133000 SUMMARY: Rick Erkens: “Rewriting the Term Rewriter Part 1: Introduction and Matching” DESCRIPTION: In an mCRL2 specification the user can specify processes with data\, that can in turn be manipulated through the computational model of t erm rewriting. The term rewriter that the toolset uses now is reasonably fa st ...continue reading XALTDESC;FMTTYPE=text/html:Parity games are twoplayer\, infinite dur ation games that can be used answer whether a property holds true of a syst em with a yes or no. In several application domains\, one is not only inter ested in a yes/no answer\, but in computing some/all values to parameters i n a system description for which a property holds true. A naive approach to this problem involves solving many parity games. In the hope of taking adv antage of structural commonalities among a collection of games\, thus avoid ing many unnecessary computations\, we introduce variability parity games a s a generalisation of parity games. We will briefly discuss an algorithm th at directly solves such variability parity games. As a motivation for\, and an application of the developed theory\, we suggest how it can be used in the setting of Software Product Lines for modal mucalculus model checking for Featured Transition Systems. This is very much work in (slow) progress. ..
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/timwillemsevariability paritygames/ END:VEVENT BEGIN:VEVENT UID:20190320T1319Z1553087999.2203EO5311@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190320T093442Z LASTMODIFIED:20190320T093442Z DTSTART;TZID=Europe/Amsterdam:20190321T124500 DTEND;TZID=Europe/Amsterdam:20190321T133000 SUMMARY: Jurriaan Rot: Coalgebra Learning via Duality DESCRIPTION: Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We generalise learnin g from automata to a large class of statebased systems\, using the theory of coalgebras. The approach relies ...continue reading XALTDESC;FMTTYPE=text/html:Automata learning is a popular technique f
or inferring minimal
automata through membership and equivalence queri
es. We generalise
learning from automata to a large class of statebas
ed systems\, using
the theory of coalgebras. The approach relies on th
e use of logical
formulas as tests\, based on a dual adjunction betwee
n states and
logical theories. This allows us to learn\, e.g.\, labell
ed transition
systems.
Joint work with Clemens Kupke and Simone Barlocco.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/jurriaanrotcoalgebrale arningviaduality/ END:VEVENT BEGIN:VEVENT UID:20190313T1105Z1552475152.8866EO5291@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190313T103323Z LASTMODIFIED:20190313T103323Z DTSTART;TZID=Europe/Amsterdam:20190314T124500 DTEND;TZID=Europe/Amsterdam:20190314T133000 SUMMARY: Olav Bunte: “Formalising the semantics of OIL: the first steps” DESCRIPTION: In the last years an increasing number of companies have shown interest in applying verification techniques in model based software engin eering and Océ is one of them. To apply such techniques it is necessary to ...continue reading XALTDESC;FMTTYPE=text/html:In the last years an increasing number of companies have shown interest in applying verification techniques in model based software engineering and Océ is one of them. To apply such techniques it is necessary to have a formal semantics of the modelling language used\ , which in our case is OIL (Océ Interaction Language). We show the basic an d important ingredients of OIL and give their semantics. We also show how t he formalisation of these semantics\, using a transformation to mCRL2\, is realised.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/olavbunteformalisingth esemanticsofoilthefirststeps/ END:VEVENT BEGIN:VEVENT UID:20190226T1251Z1551185463.4125EO5181@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190226T123412Z LASTMODIFIED:20190226T123412Z DTSTART;TZID=Europe/Amsterdam:20190228T124500 DTEND;TZID=Europe/Amsterdam:20190228T133000 SUMMARY: Maurice Laveaux: Correct and Efficient Antichain Algorithms for Re finement Checking DESCRIPTION: Refinement checking plays an important role in system verifica tion. This means that the correctness of the system is established by showi ng a refinement relation between two models\; one for the implementation an d one for the ...continue reading XALTDESC;FMTTYPE=text/html:Refinement checking plays an important rol e in system verification. This means that the correctness of the system is established by showing a refinement relation between two models\; one for t he implementation and one for the specification. Previously\, Wang et al. p resented an algorithm based on antichains to efficiently decide stable fail ures refinement and failuresdivergences refinement. We have identified sev eral issues pertaining to the correctness and performance of these algorith ms and propose new\, correct\, antichainbased algorithms. Using a number o f experiments we show that our algorithms outperform the original ones in t erms of running time and memory usage.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mauricelaveauxcorrecta ndefficientantichainalgorithmsforrefinementchecking/ END:VEVENT BEGIN:VEVENT UID:20190219T1431Z1550586702.6719EO5171@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190219T125317Z LASTMODIFIED:20190219T125317Z DTSTART;TZID=Europe/Amsterdam:20190221T124500 DTEND;TZID=Europe/Amsterdam:20190221T133000 SUMMARY: Thomas Neele: Verifying SystemWide Properties of Industrial Compo nentBased Software DESCRIPTION: Analytical Software Design (ASD) enables modelbased developme nt of component software systems. Until now\, functional verification of AS D systems is only possible on a percomponent basis. There is no functional verification engine for ASD itself\, so ...continue reading XALTDESC;FMTTYPE=text/html:Analytical Software Design (ASD) enables m
odelbased development of
component software systems. Until now\, func
tional verification of ASD
systems is only possible on a percomponent
basis. There is no
functional verification engine for ASD itself\, so
this verification
relies on a translation of individual components to
mCRL2\, a
processalgebraic model checker. We show how to extend the
ASDmCRL2
translation to support multiple components in order to enabl
e checking
of system wide functional properties. With our extended tra
nslation\, we
perform a casestudy on a newly developed industrial sys
tem consisting
of 26 communicating components. The results indicate th
at it is feasible
to model check functional properties on this scale.<
/p>
CATEGORIES:Colloquium
LOCATION:MetaForum MF 7.084
GEO:51.447532;5.487437
ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl
URL;VALUE=URI:https://fsa.win.tue.nl/events/event/thomasneeleverifyingsy
stemwidepropertiesofindustrialcomponentbasedsoftware/
END:VEVENT
BEGIN:VEVENT
UID:20190213T1449Z1550069377.9378EO5141@37.128.148.44
STATUS:CONFIRMED
DTSTAMP:20190618T084143Z
CREATED:20190213T143044Z
LASTMODIFIED:20190213T143044Z
DTSTART;TZID=Europe/Amsterdam:20190214T124500
DTEND;TZID=Europe/Amsterdam:20190214T133000
SUMMARY: Alexander Fedotov: Fixing block and idle equations for FSMs in MaD
L (work in progress)
DESCRIPTION: The xMAS language introduced a convenient way of highlevel mo
deling and verification of communication fabrics. For microarchitectural m
odels expressed in xMAS\, it was shown that the problem of proving liveness
could be transformed into a ...continue reading
XALTDESC;FMTTYPE=text/html:
The xMAS language introduced a convenient way of highlevel modeling and verification of communication fabrics. For m icroarchitectural models expressed in xMAS\, it was shown that the problem of proving liveness could be transformed into a SATproblem\, which is adv antageous in terms of scalability. Later on\, Verbeek et al. proposed an ap proach to combine basic xMAS primitives with Finite State Machines. The ide a itself resulted in a more expressive\, yet scalable technique for modelin g and verification of microarchitectures. However\, we found a mistake in i t. In the current work\, we show that the technique introduced by Verbeek e t al. is not sound\, i.e.\, it fails to prove deadlock freedom. We propose a new method which addresses the problems of the previous approach.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/alexanderfedotovfixing blockandidleequationsforfsmsinmadlworkinprogress/ END:VEVENT BEGIN:VEVENT UID:20190206T0931Z1549445506.2991EO5121@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190206T082009Z LASTMODIFIED:20190206T082009Z DTSTART;TZID=Europe/Amsterdam:20190207T124500 DTEND;TZID=Europe/Amsterdam:20190207T133000 SUMMARY: Erik de Vink: On a complete axiomatization of rooted branching pro babilistic bisimulation DESCRIPTION: We consider a process language featuring both nondeterministic and probabilistic choice with an operational semantics taking distribution s of processes as basic building blocks. For this langauge we propose a sou nd and complete axiomatization of rooted ...continue reading XALTDESC;FMTTYPE=text/html:We consider a process language featuring b
oth nondeterministic and
probabilistic choice with an operational sema
ntics taking
distributions of processes as basic building blocks. For
this langauge
we propose a sound and complete axiomatization of rooted
branching
probabilistic bisimulation. Exploiting the notion of a conc
rete
process and building on the completeness of strong probabilistic<
br />bisimulation\, a completeness result for rooted branching probabilisti
c
bisimulation is obtained.
Joint work with Jan Friso Groote
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/erikdevinkonacomplet eaxiomatizationofrootedbranchingprobabilisticbisimulation/ END:VEVENT BEGIN:VEVENT UID:20190131T1923Z1548962620.691EO5061@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190131T144556Z LASTMODIFIED:20190131T144556Z DTSTART;TZID=Europe/Amsterdam:20190205T110000 DTEND;TZID=Europe/Amsterdam:20190205T114500 SUMMARY: Mark Bouwman: A modelbased test platform for rail signalling syst ems DESCRIPTION: As technology progresses\, newer\, and more complex\, solution s are employed to verify that rail signalling systems are safe. Formal meth ods provide ways to increase rigour in the verification process. This preci sion\, accompanied by the ongoing ...continue reading XALTDESC;FMTTYPE=text/html:As technology progresses\, newer\, and mor e complex\, solutions are employed to verify that rail signalling systems a re safe. Formal methods provide ways to increase rigour in the verification process. This precision\, accompanied by the ongoing increase of computati onal power of computers\, also opens up ways to partially automate parts of the verification process. We present a case study an application of mCRL2 and the modelbased testing tool JTorX in the signalling domain. The mCRL2 toolkit is used to formally model the behaviour of a system at the core of signalling solutions: the interlocking. The behaviour of the interlocking i s validated through model checking\, proving that relevant safety propertie s hold. Using JTorX\, the formal model is turned into the benchmark in an a utomated testing platform for interlocking software. A working setup with a ctual interlocking software on a preexisting testing platform is presented \, though performance and stability remain an issue. The suitability of mCR L2 and JTorX in the signalling domain is evaluated and suggestions are give n for improvement and further research.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 3 GEO:51.447567;5.487443 ORGANIZER;CN="Bas Luttik":MAILTO:s.p.luttik@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/markbouwmanamodelbase dtestplatformforrailsignallingsystems/ END:VEVENT BEGIN:VEVENT UID:20190129T2122Z1548796927.4215EO5021@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190129T135403Z LASTMODIFIED:20190129T135403Z DTSTART;TZID=Europe/Amsterdam:20190131T124500 DTEND;TZID=Europe/Amsterdam:20190131T131500 SUMMARY: Bas Luttik: Revised Semantics for Sequential Composition in the Pr esence of Intermediate Acceptance DESCRIPTION: For a smooth integration of classical automata theory and conc urrency theory\, one would like to consider process algebras including a co nstant denoting successful termination and binary operations for alternativ e and sequential composition. Using alternative composition ...continue rea ding XALTDESC;FMTTYPE=text/html:For a smooth integration of classical auto mata theory and concurrency theory\, one would like to consider process alg ebras including a constant denoting successful termination and binary opera tions for alternative and sequential composition. Using alternative composi tion and successful termination it is possible to express a notion of inter mediate acceptance as it occurs\, e.g.\, in (classical) finite automata. Se quential composition is necessary for the processtheoretic counterpart of contextfree grammars. A process algebra including said ingredients with th eir traditional semantics\, however\, also inherits the less desirable phen omenon of transparency: behaviour of the first component of a sequential co mposition may be skipped.
We present a revised semantics for sequenti al composition that retains the properties needed for a smooth integration of classical automata theory and concurrency theory\, but eliminates transp arency. For the resulting process algebra we have obtained axiomatisation a nd decidability results.
(based on joint work with Jos Baeten\, Astri d Belder and Fei Yang)
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/basluttikrevisedsemant icsforsequentialcompositioninthepresenceofintermediateacceptance/ END:VEVENT BEGIN:VEVENT UID:20190115T1415Z1547561732.4671EO4901@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190115T063254Z LASTMODIFIED:20190115T063254Z DTSTART;TZID=Europe/Amsterdam:20190117T124500 DTEND;TZID=Europe/Amsterdam:20190117T131500 SUMMARY: Hans Zantema: Equational reasoning\, induction\, and infinite data structures DESCRIPTION: Inductive theorem proving combines equational reasoning and in duction to prove properties on ground terms. We present some basics\, and s how how it also applies in data structures not having a unique representati on and in infinite ...continue reading XALTDESC;FMTTYPE=text/html:Inductive theorem proving combines equatio nal reasoning and induction to prove properties on ground terms. We present some basics\, and show how it also applies in data structures not having a unique representation and in infinite data structures.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hanszantemaequationalr easoninginductionandinfinitedatastructures/ END:VEVENT BEGIN:VEVENT UID:20190109T0230Z1547001003.7325EO4881@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20190108T152049Z LASTMODIFIED:20190108T152049Z DTSTART;TZID=Europe/Amsterdam:20190110T124500 DTEND;TZID=Europe/Amsterdam:20190110T131500 SUMMARY: Sofie Haesaert: Robust Dynamic Programming for Temporal Logic Cont rol of Stochastic Systems DESCRIPTION: Discretetime stochastic systems are an essential modelling to ol for many engineering systems. We consider stochastic control systems tha t are evolving over continuous spaces. For this class of models\, methods f or the formal verification and synthesis ...continue reading XALTDESC;FMTTYPE=text/html:Discretetime stochastic systems are an es sential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class o f models\, methods for the formal verification and synthesis of control str ategies are computationally hard and generally rely on the use of approxima te abstractions. Building on approximate abstractions\, we compute control strategies with lower and upperbounds for satisfying unbounded temporal l ogic specifications. Firstly\, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verifica tion problem. These mappings yield a control strategy and a unique lower bo und on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Secondly\, upperbounds on the satisfaction probability are quantified\, and properties of the mapping s are analysed and discussed. Finally\, we show the implications of these r esults for linear stochastic dynamic systems with a continuous state space. This abstractionbased synthesis framework is shown to be able to handle i nfinitehorizon properties. Approximation errors expressed as deviations in the outputs of the models and as deviations in the probabilistic transitio ns are allowed and are quantified using approximate stochastic simulation r elations.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/sofiehaesaertrobustdyn amicprogrammingfortemporallogiccontrolofstochasticsystems/ END:VEVENT BEGIN:VEVENT UID:20181219T0034Z1545179699.8399EO4861@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181218T150540Z LASTMODIFIED:20181218T150540Z DTSTART;TZID=Europe/Amsterdam:20181220T124500 DTEND;TZID=Europe/Amsterdam:20181220T131500 SUMMARY: Maciej Gazda: Logical characterisation of hybrid conformance DESCRIPTION: The notion of conformance provides a rigorous basis for testin g systems. In particular\, a notion of hybrid conformance is useful in esta blishing a formal modelbased technique for cyberphysical systems. A logic al characterisation of conformance precisely ...continue reading XALTDESC;FMTTYPE=text/html:The notion of conformance provides a rigor
ous basis for testing
systems. In particular\, a notion of hybrid conf
ormance is useful in
establishing a formal modelbased technique for c
yberphysical
systems. A logical characterisation of conformance preci
sely specifies
the set of formulae that are preserved and reflected by
conformance.
We present what is to our knowledge\, the first characte
risation result
for an approximate notion of hybrid conformance. To th
is end\, we show
that the relaxation scheme used for preservation resu
lts in this
setting is not tight enough for providing a characterisati
on and
propose a tighter relaxation that we subsequently prove to be t
he
right one for characterising hybrid conformance.
In this talk\, first I give an overview of activities in our session type group in Imperial and how mCRL2 is used in our researches.
Go is a productionlevel statically typed programming language whose design features explicit messagepassing primitives and lig htweight threads\, enabling (and encouraging) programmers to develop concur rent systems where components interact through communication more so than b y lockbased shared memory concurrency. Go can detect global deadlocks at r untime\, but does not provide any compiletime protection against all too c ommon communication mismatches and partial deadlocks.
In this work\, we present a static verification framework for liveness and safety in Go pr ograms\, able to detect communication errors and deadlocks by mCRL2. Our to olchain infers from a Go program a faithful representation of its communica tion patterns as behavioral types\, where the types are model checked for l iveness and safety.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/nobukoyoshidabehavioura ltypebasedstaticverificationframeworkforgo/ END:VEVENT BEGIN:VEVENT UID:20181204T1553Z1543938796.7268EO4811@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181204T140617Z LASTMODIFIED:20181204T140617Z DTSTART;TZID=Europe/Amsterdam:20181206T124500 DTEND;TZID=Europe/Amsterdam:20181206T131500 SUMMARY: Muhammad Osama: SAT Solving using Ant Colony Optimization on GPUs DESCRIPTION: In this talk\, I will discuss how the Boolean Satisfiability ( SAT) problem can be solved using a parallel implementation of the Ant Colon y Optimization (ACO) algorithm for execution on the Graphics Processing Uni t (GPU). We ...continue reading XALTDESC;FMTTYPE=text/html:In this talk\, I will discuss how the Bool ean Satisfiability (SAT) problem can be solved using a parallel implementat ion of the Ant Colony Optimization (ACO) algorithm for execution on the Gra phics Processing Unit (GPU). We propose a new efficient parallel strategy f or the ACO algorithm executed entirely on the CUDA architecture\, and perfo rm experiments to compare it with the best sequential version exists implem ented on CPU with incomplete approaches. We show how SAT problem can benefi t from the GPU solutions\, leading to significant improvements in speedup even though keeping the quality of the solution. Our results shows that the new parallel implementation executes up to 21x faster compared to its sequ ential counterpart.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/muhammadosamasatsolvin gusingantcolonyoptimizationongpus/ END:VEVENT BEGIN:VEVENT UID:20181128T1936Z1543433796.8335EO4801@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181128T131041Z LASTMODIFIED:20181128T131041Z DTSTART;TZID=Europe/Amsterdam:20181129T124500 DTEND;TZID=Europe/Amsterdam:20181129T131500 SUMMARY: Anton Wijs: The SLCO Framework for Verified\, Modeldriven Constru ction of Component Software DESCRIPTION: I will present the Simple Language of Communicating Objects (\ \SLCO) framework\, which has resulted from our research on applying formal methods for correct and efficient modeldriven development of multicompone nt software. At the core is a ...continue reading XALTDESC;FMTTYPE=text/html:I will present the Simple Language of Comm unicating Objects (\\SLCO) framework\, which has resulted from our research on applying formal methods for correct and efficient modeldriven developm ent of multicomponent software. At the core is a domain specific language called SLCO that can be used to specify software behaviour. One of the feat ures of the framework is the formal verification of SLCO models\, which is provided via a translation to mCRL2. In this talk\, I will discuss the lang uage SLCO\, give an overview of the features of the framework\, and discuss our roadmap for the future.
CATEGORIES:Colloquium LOCATION:MetaForum MF 6.131 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/antonwijstheslcoframe workforverifiedmodeldrivenconstructionofcomponentsoftware/ END:VEVENT BEGIN:VEVENT UID:20181121T1807Z1542823679.1154EO4751@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181121T093528Z LASTMODIFIED:20181121T093528Z DTSTART;TZID=Europe/Amsterdam:20181122T124500 DTEND;TZID=Europe/Amsterdam:20181122T131500 SUMMARY: Jan Friso Groote: A game that I can win\, but don’t know how DESCRIPTION: After the PhD. defense of Maciej Gazda\, I walked back with on e of the committee members who explained me a game that he knew he could wi n\, but he would not be able to tell ...continue reading XALTDESC;FMTTYPE=text/html:After the PhD. defense of Maciej Gazda\, I
walked back with one of the committee members
who explained me a game
that he knew he could win\, but he would not be able to tell how.
At ASML the ASOME data modelling language has been defined. Many system designers are defining models in this languag e\, and the question is whether there is an easy way to assess that these m odels are ok. This can be done using metrics. The question is which metrics are proper. In this MSc research various metrics from different sources ar e collected. The suitability of these metrics to indicate the complexity an d maintainability of the models is assessed by questionaires and qualitati ve interviews.
CATEGORIES:MSc Defence LOCATION:Metaforum MF3.122 GEO:52.374540;4.897976 ORGANIZER;CN="Jan Friso Groote":MAILTO:j.f.groote@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hongzhangqualitymetric sforasomedatamodels/ END:VEVENT BEGIN:VEVENT UID:20181114T1259Z1542200383.5658EO4711@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181114T101903Z LASTMODIFIED:20181114T101903Z DTSTART;TZID=Europe/Amsterdam:20181115T124500 DTEND;TZID=Europe/Amsterdam:20181115T131500 SUMMARY: M. Laveaux\, T. Neele\, O. Bunte: The 201808.0 mCRL2 release DESCRIPTION: In this talk\, we will give an overview of the additions and i mprovements to mCRL2 from the last couple of years. First\, the mCRL2 langu age has been expanded with the possibility to specify probabilistic behavio ur. ...continue reading XALTDESC;FMTTYPE=text/html:In this talk\, we will give an overview of the additions and improvements to mCRL2 from the last couple of years. Fir st\, the mCRL2 language has been expanded with the possibility to specify p robabilistic behaviour. Second\, there are several new and improved impleme ntations of behavioural relations: the GJKW algorithm for branching bisimul ation with complexity O(m log n)\, several new preorders and an implementat ion of probabilistic branching bisimulation. Model checking with the modal mucalculus has been expanded with the possibility to generate evidence in the form of a counterexample or witness. Furthermore\, there are some new techniques to support model checking of infinitestate systems. Finally\, t here is a new\, more intuitive tool for developing specifications. This too l is called mCRL2ide and it support visualisation of state spaces and also model checking of mucalculus properties. Throughout the talk\, we will do several demos.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mlaveauxtneeleobunte the2018080mcrl2release/ END:VEVENT BEGIN:VEVENT UID:20181107T1041Z1541587292.6296EO4671@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181107T101005Z LASTMODIFIED:20181107T101005Z DTSTART;TZID=Europe/Amsterdam:20181108T124500 DTEND;TZID=Europe/Amsterdam:20181108T131500 SUMMARY: Rick Erkens: Upto Techniques for Branching Bisimulation DESCRIPTION: Branching bisimilarity is a notion of behavioral equivalence b etween processes. To prove that two processes are branching bisimilar one s hould provide a relation (a set of pairs) containing the two processes\, su ch that the relation ...continue reading XALTDESC;FMTTYPE=text/html:Branching bisimilarity is a notion of beha vioral equivalence between processes. To prove that two processes are branc hing bisimilar one should provide a relation (a set of pairs) containing th e two processes\, such that the relation satisfies some properties. For rec ursive processes this relation often becomes infinite and complicated\, whi ch may lead to awkward and long proofs. We discuss improvements of the bran ching bisimulation proof technique that are based on the socalled 'upto t echniques' that already exist for strong and weak bisimulation.
CATEGORIES:Colloquium LOCATION:MetaForum MF 11 GEO:0;0 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rickerkensuptotechniq uesforbranchingbisimulation/ END:VEVENT BEGIN:VEVENT UID:20181101T1019Z1541067594.7602EO4551@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181031T161025Z LASTMODIFIED:20181031T161522Z DTSTART;TZID=Europe/Amsterdam:20181107T140000 DTEND;TZID=Europe/Amsterdam:20181107T144500 SUMMARY: Ferry Timmers: A complete axiomatisation for probabilistic trace e quivalence DESCRIPTION: In the thesis a complete axiomatisation is given for probabili stic trace equivalence for finite\nprocesses. The axiomatisation is remarka bly complex\, which may explain that nobody formulated\nsuch a complete axi omatisation yet. XALTDESC;FMTTYPE=text/html:In the thesis a sound and complete axiomat isation is given for probabilistic trace equivalence for finite probabilist ic processes. The axiomatisation is remarkably complex\, which may explain that nobody formulated such a complete axiomatisation yet.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 4 GEO:0;0 ORGANIZER;CN="Jan Friso Groote":MAILTO:j.f.groote@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ferrytimmersacomplete axiomatisationforprobabilistictraceequivalence/ END:VEVENT BEGIN:VEVENT UID:20181024T2029Z1540412980.2235EO4511@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181024T060351Z LASTMODIFIED:20181025T140007Z DTSTART;TZID=Europe/Amsterdam:20181025T133000 DTEND;TZID=Europe/Amsterdam:20181025T150000 SUMMARY: Mahmoud Talebi: Scalable performance analysis of wireless sensor n etworks XALTDESC;FMTTYPE=text/html: CATEGORIES:PhD Defence LOCATION:Auditorium\, Senaatzaal GEO:0;0 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mahmoudtalebiscalablep erformanceanalysisofwirelesssensornetworks/ END:VEVENT BEGIN:VEVENT UID:20181017T1832Z1539801161.1166EO4481@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20181017T170642Z LASTMODIFIED:20181017T170642Z DTSTART;TZID=Europe/Amsterdam:20181018T124500 DTEND;TZID=Europe/Amsterdam:20181018T131500 SUMMARY: Dragan Bosnacki: Analysis of a Boolean Model for Rheumatoid Arthri tis Using SMTSolvers DESCRIPTION: Rheumatoid Arthritis (RA) is an autoimmune disease that affect s about one percent of the world population. A medicine for RA has not yet been found\, current treatment options only decelerating the progress of th e disease. ...continue reading XALTDESC;FMTTYPE=text/html:Rheumatoid Arthritis (RA) is an autoimmune
disease that affects about
one percent of the world population. A med
icine for RA has not yet been
found\, current treatment options only d
ecelerating the progress of the
disease. In this work a Boolean networ
k model for RA is analysed. Two
kinds of models\, synchronous and asyn
chronous are compared. Attractors
in the state space of the models are
identified that correspond to the
steady states and stable cycles of
the network. To this end
Satisfiability Modulo Theory (SMT) solvers an
d an adaptation of the
Tarjan’s algorithm for finding strongly connect
ed components in a graph
are used for the synchronous and asynchronous
models\, respectively. By
analysing the stability of the network nod
es potential drug targets are
identified. The results show a significa
nt overlap with similar findings
in the literature which indicates tha
t the Boolean networks can be a
feasible approach for identifying biom
arkers and drug targets.
We discuss an extension of the coordinatio
n modelling language
Paradigm. The extension is geared towards datade
pendent interaction
among components\, where the coordination is influ
enced by possibly
distributed data. The approach is illustrated by the
wellknown
example of a bakery where tickets are issued to serve clie
nts in
order. Also\, it is described how to encode Paradigm models wit
h data
in the process language of the mCRL toolset for further analysi
s
of the coordination.
Parity games are two player games with ome gawinning conditions\, played on finite graphs. Such games play an importa nt role in verification\, satisfiability and synthesis. It is therefore imp ortant to identify algorithms that can efficiently deal with large games th at arise from such applications. In this paper\, we describe our experiment s with BDDbased implementations of four parity game solving algorithms\, v iz. Zielonka’s recursive algorithm\, the more recent Priority Promotion alg orithm\, the FixpointIteration algorithm and the automata based APT algori thm. We compare their performance on several types of random games and on a number of cases taken from the Keiren benchmark set.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/timwillemseacomparison ofbddbasedparitygamesolversjointworkwithlisettesanchezandwiege rwesselink/ END:VEVENT BEGIN:VEVENT UID:20180924T1715Z1537809323.5069EO4381@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180924T134455Z LASTMODIFIED:20180924T134455Z DTSTART;TZID=Europe/Amsterdam:20180927T124500 DTEND;TZID=Europe/Amsterdam:20180927T131500 SUMMARY: Thomas Neele: Fixing mistakes: narrowing the scope of quantifiers in PBESs DESCRIPTION: In the mCRL2 toolset\, formal properties are specified in the modal mucalculus with data. This formalism allows the use of quantifiers ( ∀ and ∃) to bind data variables. However\, when a user puts a quantifier .. .continue reading XALTDESC;FMTTYPE=text/html:In the mCRL2 toolset\, formal properties a re specified in the modal mucalculus with data. This formalism allows the use of quantifiers (∀ and ∃) to bind data variables. However\, when a user puts a quantifier in the wrong place\, our current set of tools maybe unabl e to solve the resulting model checking problem. An example of such a poorl y written property is ∀d:D.[true*.drop(d)]false. In this talk\, I will show an automated technique to fix such errors. We perform the analysis on the level of parameterised Boolean equation systems (PBESs)\, that encode the c ombination of a model and a property.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.209 GEO:0;0 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/thomasneelefixingmista kesnarrowingthescopeofquantifiersinpbess/ END:VEVENT BEGIN:VEVENT UID:20180919T1138Z1537357087.0224EO4331@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180919T060628Z LASTMODIFIED:20180919T060749Z DTSTART;TZID=Europe/Amsterdam:20180920T124500 DTEND;TZID=Europe/Amsterdam:20180920T131500 SUMMARY: Joel Garcia: Behavioural modelling of a wafer transport unit using mCRL2 DESCRIPTION: As a master’s student I’m doing an internship with the assigne ment to design a model for an ASML wafer transport unit. The objective is t o model the behaviour of two stages of the wafer transport ...continue read ing XALTDESC;FMTTYPE=text/html:As a master’s student I'm doing an interns hip with the assignement to design a model for an ASML wafer transport unit . The objective is to model the behaviour of two stages of the wafer transp ort unit: the wafer hanlder and the wafer stage. The model of such a machin e is built by using the mCRL2 language. In this presentation\, I will expla in the progress of the work I have so far.
CATEGORIES:Colloquium LOCATION:MetaForum MF 3 GEO:51.447567;5.487443 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/joelgarciabehaviouralm odellingofawafertransportunitusingmcrl2/ END:VEVENT BEGIN:VEVENT UID:20180913T0718Z1536823131.2466EO4191@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180912T095905Z LASTMODIFIED:20180912T095905Z DTSTART;TZID=Europe/Amsterdam:20180913T124500 DTEND;TZID=Europe/Amsterdam:20180913T131500 SUMMARY: Omar Alduhaiby: Learning Product Automata DESCRIPTION: Following a discussion with my colleague at University of Radb oud Joshua Moerman on learning the product of independent automata\, he pur sued the subject of independence of outputs while I the independence of inp uts. In this ...continue reading XALTDESC;FMTTYPE=text/html:Following a discussion with my colleague a t University of Radboud Joshua Moerman on learning the product of independe nt automata\, he pursued the subject of independence of outputs while I the independence of inputs. In this presentation I will summarise his recent p aper titled ‘Learning Product Automata’ and how it relates to my work. I wi ll present an example of a system under learning and demonstrate how its ou tput is an aggregation of a several independent outputs. The system is then separated into those smaller subsystem units\, and a modification on the l earning algorithm learns those subsystems and performs a Cartesian product on them to output the complete system’s automaton\, thus by optimizing on t he learning time. We then view the practical results from the paper and dis cuss how fruitful my approach would be.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/omaralduhaibylearningp roductautomata/ END:VEVENT BEGIN:VEVENT UID:20180905T0249Z1536115777.6308EO4061@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180904T204326Z LASTMODIFIED:20180904T204326Z DTSTART;TZID=Europe/Amsterdam:20180906T124500 DTEND;TZID=Europe/Amsterdam:20180906T131500 SUMMARY: Julien Schmaltz: On the definition of block and idle for xMAS auto mata. DESCRIPTION: xMAS is a language initially proposed by Intel for architectur al modelling and verification. The main feature of xMAS is to enable a bool ean encoding of liveness that can be efficiently checked using SATbased te chniques. xMAS ...continue reading XALTDESC;FMTTYPE=text/html:xMAS is a language initially proposed by I ntel for architectural modelling and verification. The main feature of xMAS is to enable a boolean encoding of liveness that can be efficiently checke d using SATbased techniques. xMAS is restricted to a small set of welldef ined primitives. Recently\, Verbeek et al. extended this approach to state machines. In this talk\, I will recall the definitions they propose for the main boolean variables (block and idle) of the encoding. I will then show two counterexamples to these definition. Together with Alexander\, we are currently working on fixing these definitions. I will discuss our current h int. This will be quite sketchy as we do not really have a satisfactory sol ution yet.
CATEGORIES:Colloquium LOCATION:MetaForum MF 12 GEO:0;0 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/julienschmaltzonthede finitionofblockandidleforxmasautomata/ END:VEVENT BEGIN:VEVENT UID:20180808T2033Z1533760408.1177EO3891@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180808T130322Z LASTMODIFIED:20180813T135934Z DTSTART;TZID=Europe/Amsterdam:20180814T160000 DTEND;TZID=Europe/Amsterdam:20180814T164500 SUMMARY: Lisette Sanchez: Learning software behavior through active automat a learning with data DESCRIPTION: The topic of the thesis is find out whether the LS* learning a lgorithm\, that can learn register automata with abstract data parameters f rom actual software is practically applicable in an industrial context. The algorithm can ...continue reading XALTDESC;FMTTYPE=text/html:The topic of the thesis is find out whethe r the LS* learning algorithm\, that can learn register automata with abstra ct data parameters from actual software is practically applicable in an ind ustrial context. The algorithm can for instance learn a queue with limited size that stores arbitrary natural numbers.
The conclusion is that i ndeed practical software can be learned\, outperforming the learning of aut omata with concrete data. Scale remains a problem\, though.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 13 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/lisettesanchezlearning softwarebehaviorthroughactiveautomatalearningwithdata/ END:VEVENT BEGIN:VEVENT UID:20180718T0944Z1531907068.7232EO3771@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180718T091528Z LASTMODIFIED:20180718T091528Z DTSTART;TZID=Europe/Amsterdam:20180724T100000 DTEND;TZID=Europe/Amsterdam:20180724T104500 SUMMARY: Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum DESCRIPTION: Van Glabbeek presented the linear time – branching time spectr um of behavioural semantics and gave sound\, groundcomplete axiomatisation s for the process theory BCCSP. Groote and Chen et al. proved for the seman tics in the spectrum ...continue reading XALTDESC;FMTTYPE=text/html:Van Glabbeek presented the linear time  b ranching time spectrum of behavioural semantics and gave sound\, groundcom plete axiomatisations for the process theory BCCSP. Groote and Chen et al. proved for the semantics in the spectrum whether there exist finite axiomat isations that are omegacomplete. We add termination and sequential composi tion to the spectrum by studying the semantics for the process theories BSP and TSP. We provide a template for proving soundness and groundcompletene ss for BSP and apply this template to BSP modulo trace semantics. We prove that for BSP modulo ready simulation semantics with a finite number of acti ons of at least one a finite basis does not exist by giving an infinite fam ily of equations which are sound but cannot be derived from a finite collec tion of axioms that are sound for BSP modulo ready simulation semantics. We show that we cannot use this family of equations to prove whether TSP modu lo ready simulation semantics affords a finite basis. Finally\, we prove th at TSP modulo bisimulation is omegacomplete when there is at least one act ion.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 14 GEO:51.447532;5.487437 ORGANIZER;CN="Bas Luttik":MAILTO:s.p.luttik@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/loisnijlandaddingseque ntialcompositionandterminationtothelineartimebranchingtimespectru m/ END:VEVENT BEGIN:VEVENT UID:20180717T1144Z1531827868.9545EO3761@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180717T095712Z LASTMODIFIED:20180717T095712Z DTSTART;TZID=Europe/Amsterdam:20180723T150000 DTEND;TZID=Europe/Amsterdam:20180723T154500 SUMMARY: Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination DESCRIPTION: An alternative semantics for sequential composition in a setti ng with intermediate termination was proposed in a recent article by Baeten \, Luttik and Yang. We consider two open questions regarding sequential pro cesses with intermediate termination that ...continue reading XALTDESC;FMTTYPE=text/html:An alternative semantics for sequential co mposition in a setting with intermediate termination was proposed in a rece nt article by Baeten\, Luttik and Yang. We consider two open questions rega rding sequential processes with intermediate termination that use the revis ed semantics for sequential composition (TSP^{\;}). First\, a groun dcomplete axiomatisation is proposed for TSP^{\;}\, extended with an auxiliary operator that is used to remove intermediate termination from terms. Additionally\, it is shown that TSP^{\;} does not afford a g roundcomplete axiomatisation with respect to bisimilarity without an auxil iary operator. Second\, we prove that bisimilarity is decidable for process es definable by finite guarded recursive specification over TSP^{\;}. This is done by showing that every guarded recursive TSP^{\;}sp ecification can be transformed to a normal form\, which allows us to elimin ate redundant intermediate termination from processes. Using this normal fo rm\, the existing decidability proofs for contextfree processes without in termediate termination\, can be adapted for TSP^{\;}.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 14 GEO:51.447532;5.487437 ORGANIZER;CN="Bas Luttik":MAILTO:s.p.luttik@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/astridbelderdecidabilit yofbisimilarityandaxiomatisationforsequentialprocessesinthepresen ceofintermediatetermination/ END:VEVENT BEGIN:VEVENT UID:20180704T0251Z1530672715.5931EO3671@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180703T125022Z LASTMODIFIED:20180703T125022Z DTSTART;TZID=Europe/Amsterdam:20180705T124500 DTEND;TZID=Europe/Amsterdam:20180705T133000 SUMMARY: Tatiana Shmeleva: Modeling Networks with Infinite Petri Nets DESCRIPTION: A composition and analysis technique is developed for investig ation of infinite Petri nets with regular structure\, introduced for modeli ng networks\, clusters and computing grids\, that also concerns cellular au tomata and biological systems. A case study ...continue reading XALTDESC;FMTTYPE=text/html:A composition and analysis technique is de veloped for investigation of infinite Petri nets with regular structure\, i ntroduced for modeling networks\, clusters and computing grids\, that also concerns cellular automata and biological systems. A case study of a square grid structure composition and analysis is presented. Parametric specifica tion of Petri nets\, parametric representation of infinite systems for the calculation of place/transition invariants\, and solving them in parametric form allowed the invariance proof for infinite Petri net models. Some addi tional analysis techniques based on graphs of transmissions and blockings a re presented. Further generalization on multidimensional structures such as hypercube and hypertorus have been implemented. Generators of Petri net mo dels have been developed and put on GitHub for public use. Complex deadlock s are disclosed and a possibility of network blocking via illintentioned t raffic revealed. Quality of service in modern networks and numerical parame ters of blocking networks with disguised illintentioned traffic are invest igated using reenterable models in the form of colored Petri nets.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/tatianashmelevamodeling networkswithinfinitepetrinets/ END:VEVENT BEGIN:VEVENT UID:20180702T1919Z1530559177.5363EO3661@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180702T173658Z LASTMODIFIED:20180708T174452Z DTSTART;TZID=Europe/Amsterdam:20180702T100000 DTEND;TZID=Europe/Amsterdam:20180702T104500 SUMMARY: Marijn Rol: Verification of ASD multicomponent systems in mCRL2 DESCRIPTION: Analytical Software Design (ASD) assists the creation of softw are systems. Systems designed in ASD are composed of multiple components in order to divide the complexity of the whole system over them. The verifica tion of system ...continue reading XALTDESC;FMTTYPE=text/html:Analytical Software Design (ASD) assists t he creation of software systems. Systems designed in ASD are composed of mu ltiple components in order to divide the complexity of the whole system ove r them. The verification of system properties and requirements is limited t o the scope of single components\, disallowing the verification of endtoe nd properties. We present an approach for the verification of endtoend pr operties on multicomponent systems. This provides a higher confidence in t he functional correctness and reliability. A system based on a reallife AS D model serves as usecase for the proposed approach. Results show that ver ification of multicomponent systems can be done through mCRL2\, but scalab ility issues are observed as larger systems are verified.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 13 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/marijnrolverificationo fasdmulticomponentsystemsinmcrl2/ END:VEVENT BEGIN:VEVENT UID:20180626T1000Z1530007224.222EO3641@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180626T092822Z LASTMODIFIED:20180626T092822Z DTSTART;TZID=Europe/Amsterdam:20180628T124500 DTEND;TZID=Europe/Amsterdam:20180628T133000 SUMMARY: Maurice Laveaux: Verification in mCRL2 using multithreaded algori thms: The term library. DESCRIPTION: Currently the mCRL2 toolset uses sequential algorithms exclusi vely. From these sequential algorithms the term rewriting algorithm often h as the most prominent runtime cost. Developing a parallel term rewriting a lgorithm requires an efficient term library. This ...continue reading XALTDESC;FMTTYPE=text/html:Currently the mCRL2 toolset uses sequentia l algorithms exclusively. From these sequential algorithms the term rewriti ng algorithm often has the most prominent runtime cost. Developing a paral lel term rewriting algorithm requires an efficient term library. This libra ry facilitates the creation and destruction of terms. In this presentation I will present several challenges that I encountered while trying to develo p an efficient term library. Followed by several observations that lead to an envisioned design for a parallel term rewriting algorithm.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mauricelaveauxverificat ioninmcrl2usingmultithreadedalgorithmsthetermlibrary/ END:VEVENT BEGIN:VEVENT UID:20180618T2021Z1529353314.2045EO3611@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180610T174747Z LASTMODIFIED:20180708T174543Z DTSTART;TZID=Europe/Amsterdam:20180611T110000 DTEND;TZID=Europe/Amsterdam:20180611T123000 SUMMARY: Fei Yang: A Theory of Executability — With a Focus on the Express ivity of Process Calculi XALTDESC;FMTTYPE=text/html: CATEGORIES:PhD Defence LOCATION:Auditorium\, Senaatzaal GEO:0;0 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/feiyangatheoryofexec utabilitywithafocusontheexpressivityofprocesscalculi/ END:VEVENT BEGIN:VEVENT UID:20180604T1504Z1528124668.0894EO3491@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180604T101812Z LASTMODIFIED:20180604T101812Z DTSTART;TZID=Europe/Amsterdam:20180607T124500 DTEND;TZID=Europe/Amsterdam:20180607T133000 SUMMARY: Hans Zantema: Making a MOOC DESCRIPTION: To make my lectures Automated Reasoning more accessible worldw ide\, I started developing a series of MOOCs (massive open online course). Professional facilities are provided by EIT Digital and Coursera. At the mo ment 21 lectures have ...continue reading XALTDESC;FMTTYPE=text/html:To make my lectures Automated Reasoning mo re accessible worldwide\, I started developing a series of MOOCs (massive o pen online course). Professional facilities are provided by EIT Digital and Coursera. At the moment 21 lectures have been recorded\, each covering aro und 10 minutes\, by which the first MOOC on satisfiability is nearly finish ed. Roughly this MOOC covers the same material on SAT/SMT as in my course A utomated Reasoning\, being around 40% of the course. In the talk this exper ience will be discussed\, in particular comparing this format with usual te aching. Also one or two of the lectures will be shown.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hanszantemamakingamoo c/ END:VEVENT BEGIN:VEVENT UID:20180530T2325Z1527722717.5901EO3431@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180530T095339Z LASTMODIFIED:20180530T095339Z DTSTART;TZID=Europe/Amsterdam:20180531T124500 DTEND;TZID=Europe/Amsterdam:20180531T133000 SUMMARY: Mahmoud Talebi: Firstorder Moment Closure Approximations for Midd leSized Systems with Nonlinear Rates DESCRIPTION: In this presentation I talk about the problem of approximating the behaviour of middlesized population models involving nonlinear rates . I describe a number of systems\, each with a very different nonlinear be haviour\, and then show ...continue reading XALTDESC;FMTTYPE=text/html:In this presentation I talk about the prob lem of approximating the behaviour of middlesized population models involv ing nonlinear rates. I describe a number of systems\, each with a very dif ferent nonlinear behaviour\, and then show that the binomial and Poisson m oment closure approximations have the potential to accurately represent the expected behaviour of these models. I then compare the two approximation m ethods to the mean field and normal moment closure approximations in terms of applicability and accuracy\, in addition to investigating their empirica l distributions\, to derive conclusions regarding their strengths and drawb acks.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mahmoudtalebifirstorde rmomentclosureapproximationsformiddlesizedsystemswithnonlinearra tes/ END:VEVENT BEGIN:VEVENT UID:20180524T0318Z1527131920.8652EO3391@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180523T140755Z LASTMODIFIED:20180523T140755Z DTSTART;TZID=Europe/Amsterdam:20180524T124500 DTEND;TZID=Europe/Amsterdam:20180524T133000 SUMMARY: Jan Friso Groote: An attempt to reap the benefits of processor ari thmetic without loosing the advantages of the numbers represented as rewrit e systems DESCRIPTION: In mCRL2 numbers are represented using rewrite systems. The re presentation is based on binary operations. This is relatively concise but far less efficient than 64 bits operations on numbers available in processo rs. I will explain ...continue reading XALTDESC;FMTTYPE=text/html:In mCRL2 numbers are represented using rew rite systems. The representation is based on binary operations. This is rel atively concise but far less efficient than 64 bits operations on numbers a vailable in processors. I will explain ongoing work towards an attempt to r eap the benefits of processor arithmetic without loosing the advantages of the numbers represented as rewrite systems.
CATEGORIES:Colloquium LOCATION:MetaForum MF 3 GEO:51.447567;5.487443 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janfrisogrooteanattem pttoreapthebenefitsofprocessorarithmeticwithoutloosingtheadvanta gesofthenumbersrepresentedasrewritesystems/ END:VEVENT BEGIN:VEVENT UID:20180516T0043Z1526431424.649EO3211@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180515T105157Z LASTMODIFIED:20180516T110034Z DTSTART;TZID=Europe/Amsterdam:20180518T100000 DTEND;TZID=Europe/Amsterdam:20180518T104500 SUMMARY: Ziad Ben Snaiba: Logics and Algorithms for Product and FamilyBase d Analysis of Software Product Lines DESCRIPTION: Most model checking techniques consider single systems. With t he rise of using Software Product Line Engineering (SPLE) for critical syst ems there is a need for model checking techniques applicable to Software Pr oduct Lines (SPL). Inspired ...continue reading XALTDESC;FMTTYPE=text/html:Most model checking techniques consider si ngle systems. With the rise of using Software Product Line Engineering (SPL E) for critical systems there is a need for model checking techniques appli cable to Software Product Lines (SPL). Inspired by Classen et al. we try to devise logics to formally describe properties suitable for the analysis of SPLs. We attempt to provide logics for both productbased and familybased model checking based on CTL. These logics allow both nested (nCTL) and sin gle (sCTL) productfamily restrictions on the specification of the SPL. Als o\, we provide an equivalence between nCTL and sCTL\, and algorithms for bo th productbased and familybased model checking using sCTL and nCTL. A sma ll toolset to use the algorithms in practice will be provided.
CATEGORIES:MSc Defence LOCATION:Flux 1.10 GEO:51.447291;5.492092 ORGANIZER;CN="Erik de Vink":MAILTO:e.p.d.vink@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ziadbensnaibalogicsan dalgorithmsforproductandfamilybasedanalysisofsoftwareproductline s/ END:VEVENT BEGIN:VEVENT UID:20180517T0431Z1526531508.0978EO3301@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180516T145617Z LASTMODIFIED:20180516T145617Z DTSTART;TZID=Europe/Amsterdam:20180517T124500 DTEND;TZID=Europe/Amsterdam:20180517T133000 SUMMARY: Bas Luttik: Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 toolset DESCRIPTION: ERTMS Hybrid Level 3 is a recent proposal for a train control system specification that serves to increase the capacity of the railway ne twork by allowing multiple trains on a single track section. We have ...con tinue reading XALTDESC;FMTTYPE=text/html:ERTMS Hybrid Level 3 is a recent proposal for a train control system specification that serves to increase the capaci ty of the railway network by allowing multiple trains on a single track sec tion.
We have formally modelled and analysed the principles of ERTMS Hybrid Level 3 in mCRL2.
Our analysis has resulted in suggestions for improvement of the principles that will be taken into account in the next version of the specification.
In this talk I’ll introduce ERTMS Hybri d Level 3\, I’ll discuss how we have obtained an mCRL2 model (or actually s everal mCRL2 models) for it\, and I’ll report on and explain some of the re sults of our analysis.
(Based on joint work with Maarten Bartholomeus and Tim Willemse.)
CATEGORIES:Colloquium LOCATION:MetaForum 3.141 GEO:51.447567;5.487443 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/basluttikmodellingand analysingertmshybridlevel3withthemcrl2toolset/ END:VEVENT BEGIN:VEVENT UID:20180502T2047Z1525294050.3391EO3141@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180502T145808Z LASTMODIFIED:20180502T145808Z DTSTART;TZID=Europe/Amsterdam:20180503T124500 DTEND;TZID=Europe/Amsterdam:20180503T133000 SUMMARY: Muhammad Osama: SIGmA: SAT Simplifications on GPU Architecture DESCRIPTION: The growing scale of industrial applications encoded to Boolea n Satisfiability (SAT) problems imposed the researchers to practice SAT sim plification as an imperative requirement for any SAT solver. In this talk\, I will discuss how GPU ...continue reading XALTDESC;FMTTYPE=text/html:The growing scale of industrial applicatio ns encoded to Boolean Satisfiability (SAT) problems imposed the researchers to practice SAT simplification as an imperative requirement for any SAT so lver. In this talk\, I will discuss how GPU can be utilized to perform vari able and subsumption eliminations in parallel. Benchmarks show that our pro posed simplifier (SIGmA) achieved an acceleration of 250x over SatELite. Re garding SAT solving\, SIGmA outperformed SatELite in terms of problems solv ed faster when combined with MiniSat by a factor of 77%. Moreover\, MiniSat was more effective than Lingeling by 73.3% in solving simplified formulas given by SIGmA.
CATEGORIES:Colloquium LOCATION:MetaForum MF 5.117 GEO:51.447567;5.487443 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/muhammadosamasigmasat simplificationsongpuarchitecture/ END:VEVENT BEGIN:VEVENT UID:20180425T2141Z1524692510.7463EO3051@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180425T164504Z LASTMODIFIED:20180425T164504Z DTSTART;TZID=Europe/Amsterdam:20180426T124500 DTEND;TZID=Europe/Amsterdam:20180426T133000 SUMMARY: Erik de Vink: On the BEM algorithm for deciding strong probabilist ic bisimulation DESCRIPTION: An algorithm for deciding strong probabilistic bisimulation\, referred to as BEM\, was proposed in 2000 by Baier\, Engelen\, and Majster Cederbaum claiming O(m n log n) complexity for the construction of the bisi mulation equivalence classes of ...continue reading XALTDESC;FMTTYPE=text/html:An algorithm for deciding strong probabili stic bisimulation\, referred to as BEM\, was proposed in 2000 by Baier\, En gelen\, and MajsterCederbaum claiming O(m n log n) complexity for the cons truction of the bisimulation equivalence classes of a probabilistic automat on. Besides socalled Ordered Balanced Trees\, the BEM algorithm uses strai ghtforward datastructures. More recently\, Groote and Rivera Verduzco propo sed an algorithm\, referred to as GRV\, of the same complexity based on mor e intricate data structures. The running times of GRV\, however\, are aroun d 1000 better than those of BEM\, on a standard set of benchmarks. Today we take a closer look at how the BEM algorithm works\, seeking explanation fo r the difference in performance compared to the GRV algorithm\, leaving GRV for another occasion.
CATEGORIES:Colloquium LOCATION:MetaForum MF 5.117 GEO:51.447567;5.487443 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/erikdevinkonthebema lgorithmfordecidingstrongprobabilisticbisimulation/ END:VEVENT BEGIN:VEVENT UID:20180411T1706Z1523466407.8255EO3011@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180411T101312Z LASTMODIFIED:20180411T101312Z DTSTART;TZID=Europe/Amsterdam:20180412T124500 DTEND;TZID=Europe/Amsterdam:20180412T133000 SUMMARY: Wieger Wesselink: Counterexamples in the mCRL2 toolset DESCRIPTION: A longstanding problem in the mCRL2 toolset was the poor supp ort for generating counterexamples of model checking properties. Over the c ourse of the last year an effort has been made to finally tackle this probl em. ...continue reading XALTDESC;FMTTYPE=text/html:A longstanding problem in the mCRL2 tools et was the poor support for generating counterexamples of model checking pr operties. Over the course of the last year an effort has been made to final ly tackle this problem. It is now possible to generate counterexamples and translate them back to the original model. The first applications of this n ew technique look very promising. In this talk I will roughly explain how t he generation of counterexamples works\, and give some examples. I will als o explain my thoughts about how to implement such an algorithm.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/wiegerwesselinkcountere xamplesinthemcrl2toolset/ END:VEVENT BEGIN:VEVENT UID:20180404T0856Z1522832197.7382EO2971@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180404T083800Z LASTMODIFIED:20180404T083800Z DTSTART;TZID=Europe/Amsterdam:20180405T124500 DTEND;TZID=Europe/Amsterdam:20180405T133000 SUMMARY: Rodin Aarsen: Static Analysis on Legacy Software DESCRIPTION: Legacy software is a prominent bottleneck in modern industry: it is hard and costly to maintain\, yet contains valuable knowledge not ava ilable elsewhere. Static analysis provides insight by extracting facts from existing code bases. In ...continue reading XALTDESC;FMTTYPE=text/html:Legacy software is a prominent bottleneck in modern industry: it is hard and costly to maintain\, yet contains valuab le knowledge not available elsewhere. Static analysis provides insight by e xtracting facts from existing code bases. In this talk\, I will address com plications and progress on my static analysis tooling in Rascal.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Mahmoud Talebi":MAILTO:m.talebi@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rodinaarsenstaticanaly sisonlegacysoftware/ END:VEVENT BEGIN:VEVENT UID:20180328T1111Z1522235509.5536EO2851@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180328T075258Z LASTMODIFIED:20180328T075258Z DTSTART;TZID=Europe/Amsterdam:20180329T124500 DTEND;TZID=Europe/Amsterdam:20180329T133000 SUMMARY: Pieter Hijma: Programming manycores with the “Stepwiserefinement for performance” methodology DESCRIPTION: The main goal of this talk is to introduce my research to the FSA group and discuss possibilities and opportunities on how this research can be combined with model checking in general and with mCRL2 ...continue r eading XALTDESC;FMTTYPE=text/html:The main goal of this talk is to introduce my research to the FSA group and discuss possibilities and opportunities o n how this research can be combined with model checking in general and with mCRL2 in particular in the context of the recently accepted TOP project AV VA (Accelerated Verification and Verified Acceleration). I will present my programming system ManyCore Levels\, the principles behind it\, and how it exposes a methodology to programmers that we call "Stepwiserefinement for performance". Manycore hardware is targeted specifically at obtaining hig h performance. However\, obtaining high performance is challenging because hardwarespecific details have to be taken into account. In our system\, pr ogrammers can define and choose their own level of abstraction: higher leve ls for readability and portability\, and userdefined lower levels to incor portate more hardwarespecific details to obtain higher performance.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/pieterhijmaprogramming manycoreswiththestepwiserefinementforperformancemethodology/ END:VEVENT BEGIN:VEVENT UID:20180323T0135Z1521768934.5068EO2771@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180321T155410Z LASTMODIFIED:20180321T155410Z DTSTART;TZID=Europe/Amsterdam:20180322T124500 DTEND;TZID=Europe/Amsterdam:20180322T133000 SUMMARY: Fei Yang: Two Problems on Contextfree Processes and Pushdown Proc esses DESCRIPTION: In this talk\, I will discuss two problems on examining in whi ch cases contextfree processes and pushdown processes are the same. In par ticular\, we depart from the wellknown case of language equivalence and in stead look ...continue reading XALTDESC;FMTTYPE=text/html:In this talk\, I will discuss two problems on examining in which cases contextfree processes and pushdown processes are the same. In particular\, we depart from the wellknown case of languag e equivalence and instead look at processes using process theory and more f inegrained equivalences\, such as branching bisimulation and contrasimulat ion. We identify two difficulties when looking at process specifications: h eadrecursion and transparency. Here two new results are achieved: we prove that when excluding transparency\, contextfree processes and pushdown pro cesses are equivalent up to at least divergenceinsensitive variant of bran ching bisimilarity. When including transparency\, we prove that they are eq uivalent up to at least contrasimulation.
This is a joint work with J os Baeten and Zeno de Hoop.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/feiyangtwoproblemson contextfreeprocessesandpushdownprocesses/ END:VEVENT BEGIN:VEVENT UID:20180314T2117Z1521062277.7493EO2721@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180314T170321Z LASTMODIFIED:20180314T170321Z DTSTART;TZID=Europe/Amsterdam:20180315T124500 DTEND;TZID=Europe/Amsterdam:20180315T133000 SUMMARY: Omar Alzuhaibi: Lessons Learned from Model Learning of Legacy Soft ware DESCRIPTION: Legacy software is one of the most common struggles of the cur rent software industry\, being costly to maintain yet essential for the ong oing industrial process. This makes refactoring especially risky. The black box reverse engineering technique ...continue reading XALTDESC;FMTTYPE=text/html:Legacy software is one of the most common struggles of the current software industry\, being costly to maintain yet e ssential for the ongoing industrial process. This makes refactoring especia lly risky. The blackbox reverse engineering technique we call model learni ng comes to aid. As pleasant in theory\, as perilous in application it is h owever. This presentation walks through some of these dangers and demonstra tes lessons I learned from analysing certain legacy components at Philips H ealthcare.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Fei Yang":MAILTO:f.yang@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/omaralzuhaibilessonsle arnedfrommodellearningoflegacysoftware/ END:VEVENT BEGIN:VEVENT UID:20180312T1759Z1520877567.5233EO2661@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180312T174345Z LASTMODIFIED:20180708T174543Z DTSTART;TZID=Europe/Amsterdam:20180313T100000 DTEND;TZID=Europe/Amsterdam:20180313T104500 SUMMARY: Ruud van Vijfeijken: Performance evaluation of network on chip usi ng formal models DESCRIPTION: Because of the increase in complexity of SystemonChip (SoC) networks by using NetworkonChip (NoC)\, latency has become a major issue in the design and validation. There are formal and mathematical methods to determine latency bounds ...continue reading XALTDESC;FMTTYPE=text/html:Because of the increase in complexity of S ystemonChip (SoC) networks by using NetworkonChip (NoC)\, latency has b ecome a major issue in the design and validation. There are formal and math ematical methods to determine latency bounds of a NoC\, such as network cal culus\, and low level simulation environments\, such as a cycleaccurate si mulation of the Register Transfer Level. This thesis proposes a method that abstracts away from low level analysis and uses a formal model to analyze the latency bounds of a given NoC. By applying different traffic schemes we can determine worst case latency of some case studies\, which include a 8 node Spidergon with cache coherency and a TornadoNoC architecture.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 3 GEO:51.447567;5.487443 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ruudvanvijfeijkenperfo rmanceevaluationofnetworkonchipusingformalmodels/ END:VEVENT BEGIN:VEVENT UID:20180308T1147Z1520509676.6478EO2601@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180308T105137Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180308T124500 DTEND;TZID=Europe/Amsterdam:20180308T133000 SUMMARY: Alexander Fedotov: Automatic Generation of Hardware Checkers from Formal Microarchitectural Specifications DESCRIPTION: To manage design complexity\, highlevel models are used to ev aluate the functionality and performance of design solutions. There is a si gnificant gap between these highlevel models and the Register Transfer Lev el (RTL) implementations actually produced ...continue reading XALTDESC;FMTTYPE=text/html:To manage design complexity\, highlevel m odels are used to evaluate the functionality and performance of design solu tions. There is a significant gap between these highlevel models and the R egister Transfer Level (RTL) implementations actually produced by designers . We address the challenge of bridging this gap\, namely\, relating abstrac t specifications to RTL implementations. An important feature of our propos ed approach is to support nondeterministic specifications. From such a non deterministic model\, we automatically compute a representation of its obs ervable behaviour. We then turn this representation into a System Verilog c hecker. The checker is connected to the input and output interfaces of the RTL implementation. The resulting combination is given to a commercial EDA tool to prove that the specification simulates the implementation. Our meth od is implemented for the formal microarchitectural description language ( MaDL) ¨C an extension of the xMAS formalism originally proposed by Intel ¨C and exemplified on several examples.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/alexanderfedotovautomat icgenerationofhardwarecheckersfromformalmicroarchitecturalspecific ations/ END:VEVENT BEGIN:VEVENT UID:20180227T1505Z1519743947.596EO2441@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180227T123012Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180301T124500 DTEND;TZID=Europe/Amsterdam:20180301T133000 SUMMARY: Thomas Neele: Proof searching in infinite parity games DESCRIPTION: One way to perform model checking of a model mucalculus formu la on a linear process is to transform the problem into a parity game. The solution to this parity game also provides an answer to ...continue reading XALTDESC;FMTTYPE=text/html:One way to perform model checking of a mod el mucalculus formula on a linear process is to transform the problem into a parity game. The solution to this parity game also provides an answer to the original model checking question. However\, for infinite systems\, suc h as realtime systems\, the parity game corresponding to most nontrivial properties is also of infinite size. To still reason about its solution\, w e developed a technique that can efficiently search for a witness or counte rexample in infinite parity games. The search is based on information cont ained in a given parameterised Boolean equation system (PBES) that encodes our model checking problem.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/thomasneeleproofsearch ingininfiniteparitygames/ END:VEVENT BEGIN:VEVENT UID:20180208T0057Z1518051434.7578EO2281@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180207T201121Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180208T124500 DTEND;TZID=Europe/Amsterdam:20180208T133000 SUMMARY: Julien Schmaltz: Formal analysis using the MaDL Whiteboard — a dem o DESCRIPTION: I will give a demo of the tool we are developing based on our research about formal analysis of microarchitectures. Going through exampl es I will illustrate the main modelling and verification features we curren tly have ...continue reading XALTDESC;FMTTYPE=text/html:I will give a demo of the tool we are deve loping based on our research about formal analysis of microarchitectures. Going through examples I will illustrate the main modelling and verificatio n features we currently have implemented. An interesting aspect is that we can model asynchronous systems. This part still requires some research and might generate some discussion :)
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/julienschmaltzformalan alysisusingthemadlwhiteboardademo/ END:VEVENT BEGIN:VEVENT UID:20180201T0356Z1517457408.1893EO2271@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180131T110544Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180201T124500 DTEND;TZID=Europe/Amsterdam:20180201T133000 SUMMARY: Hans Zantema: Some basics of SAT/SMT solving DESCRIPTION: SAT/SMT solving is a general technique for automatically findi ng solutions for a wide range of problems. In this talk some basics of the underlying techniques are presented. First we focus on SAT = satisfiability of ...continue reading XALTDESC;FMTTYPE=text/html:SAT/SMT solving is a general technique for automatically finding solutions for a wide range of problems. In this talk some basics of the underlying techniques are presented. First we focus on SAT = satisfiability of pure propositional formulas. Next we see how the sa me techniques can be extended to SMT = satisfiability modulo theories\, in particular for the theory of linear inequalities. That is\, the formulas ar e not only composed from Boolean variables and propositional operations\, b ut also from linear inequalities over numbers.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hanszantemasomebasics ofsatsmtsolving/ END:VEVENT BEGIN:VEVENT UID:20180124T0632Z1516775549.9902EO2251@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180123T171749Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180130T140000 DTEND;TZID=Europe/Amsterdam:20180130T144500 SUMMARY: Maurice Laveaux: Abstracting realvalued parameters in parameteris ed Boolean equation systems DESCRIPTION: The mCRL2 toolset utilizes parameterised boolean equation sys tems to verify formulas from modal mucalculus on models written in the min imal common representation language (mCRL2). For models of realtimed syste ms this introduces realvalued parameters in these ...continue reading XALTDESC;FMTTYPE=text/html:The mCRL2 toolset utilizes parameterised boolean equation systems to verify formulas from modal mucalculus on model s written in the minimal common representation language (mCRL2). For models of realtimed systems this introduces realvalued parameters in these equa tion systems. Solving parameterised boolean equation systems with realvalu ed parameters is not possible in most cases.
We will show that a regi on abstraction\, derived from a similar notion defined for timed automata\, can also be applied to parameterised boolean equation systems. An alternat ive abstraction where regions are combined into socalled zones will be def ined as well. In some cases this approach works better in practice. However \, it is also more restricted in the type of model checking questions that it can answer. Finally\, we will define suitable representations for region s and zones that have also been implemented using the mCRL2 language.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 14 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mauricelaveauxabstracti ngrealvaluedparametersinparameterisedbooleanequationsystems/ END:VEVENT BEGIN:VEVENT UID:20180119T1918Z1516389498.7558EO2161@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180119T082931Z LASTMODIFIED:20181031T192554Z DTSTART;TZID=Europe/Amsterdam:20180125T140000 DTEND;TZID=Europe/Amsterdam:20180125T144500 SUMMARY: Roxana Paval: Modeling and Verifying Concurrent Data Structures DESCRIPTION: Concurrent data structures can be used to communicate between parallel processes in a system. The challenge in manipulating these objects arises from the many possible ways in which the processes can interleave. To ensure correct ...continue reading XALTDESC;FMTTYPE=text/html:Concurrent data structures can be used to communicate between parallel processes in a system. The challenge in manipu lating these objects arises from the many possible ways in which the proces ses can interleave. To ensure correct executions\, the system should fulfil l linearizability. Verifying linearizability consists of checking that ever y concurrent execution is equivalent to some sequential execution that resp ects the runtime ordering of methods. This work proposes building two proce ss specifications of the object using the mCRL2 language. The concrete spec ification is built according to the implementation of the concurrent data s tructure\, while the abstract specification is linearizable by construction . Then\, linearizability can be tested by checking that their respective la beled transition systems\, generated from the mCRL2 tool\, are equivalent. This approach was applied on a number of concurrent data structures\, and i t detected both correct and faulty implementations.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 14 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/roxanapavalmodelingand verifyingconcurrentdatastructures/ END:VEVENT BEGIN:VEVENT UID:20180123T0426Z1516681567.5727EO2241@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180122T154018Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180125T124500 DTEND;TZID=Europe/Amsterdam:20180125T133000 SUMMARY: Mahmoud Talebi: Dynamic Performance Analysis of IEEE 802.15.4 Netw orks under Intermittent WiFi Transmission DESCRIPTION: The coexistence of ZigBee and WiFi networks is one of the topi cs which has been investigated both empirically and mathematically. The emp irical studies often lack scalability since the networks considered are ver y small. The mathematical ...continue reading XALTDESC;FMTTYPE=text/html:The coexistence of ZigBee and WiFi network s is one of the topics which has been investigated both empirically and mat hematically. The empirical studies often lack scalability since the network s considered are very small. The mathematical models on the other hand ofte n focus on a stable network\, ignoring he dynamic interactions of unstable systems. We provide a realtime analysis method for studying the effect of intermittent WiFi on communication in large ZigBee networks. Using our mode l we explain some of the common patterns seen in the analysis results. More over we establish that in addition to the ZigBee configuration and the clea r channel rate of WiFi\, the WiFi transmission pattern also has a high impa ct on the performance of the ZigBee network.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mahmoudtalebidynamicpe rformanceanalysisofieee802154networksunderintermittentwifitrans mission/ END:VEVENT BEGIN:VEVENT UID:20180117T0148Z1516153713.4223EO2131@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180116T185701Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180118T124500 DTEND;TZID=Europe/Amsterdam:20180118T133000 SUMMARY: Wan Fokkink: Precongruence Formats with Lookahead through Modal De composition DESCRIPTION: Bloom\, Fokkink & van Glabbeek (2004) presented a method to de compose formulas from HennessyMilner logic with regard to a structural ope rational semantics specification. A term in the corresponding process algeb ra satisfies a HennessyMilner formula if ...continue reading XALTDESC;FMTTYPE=text/html:Bloom\, Fokkink & van Glabbeek (2004) pres ented a method to decompose formulas from HennessyMilner logic with regard to a structural operational semantics specification. A term in the corresp onding process algebra satisfies a HennessyMilner formula if and only if i ts subterms satisfy certain formulas\, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this talk it is shown how this framework can be extended to specifications that include bounded l ookahead in their premises. This extension is used in the derivation of a c ongruence format for the partial trace preorder.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/wanfokkinkprecongruence formatswithlookaheadthroughmodaldecomposition/ END:VEVENT BEGIN:VEVENT UID:20180110T1111Z1515582664.262EO2081@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20180109T121457Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20180111T124500 DTEND;TZID=Europe/Amsterdam:20180111T133000 SUMMARY: Allan van Hulst: Completeness of Axioms for the Kleene Star under Bisimulation Equivalence: Some Progress DESCRIPTION: Robin Milner proposed a set of axioms for the Kleene star to c apture bisimulation equivalence. It is an open question whether this (or an y other) set of axioms is complete. I would like to take ...continue readin g XALTDESC;FMTTYPE=text/html:Robin Milner proposed a set of axioms for the Kleene star to capture bisimulation equivalence. It is an open question whether this (or any other) set of axioms is complete. I would like to tak e this opportunity to report on some progress which has been made regarding this problem: 1) It is sufficient to rewrite terms under bisimulation to s olve this problem\, 2) I have proved completeness for all cases where the s tar nesting depth is limited to two. In particular\, the first result shows that the difficulty of this problem does not lie in deriving axiomatic equ ality\, but in finding the correct normal form under bisimilarity.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/allanvanhulstcompleten essofaxiomsforthekleenestarunderbisimulationequivalencesomeprogr ess/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146518.0134EO2041@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171219T130709Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20171221T124500 DTEND;TZID=Europe/Amsterdam:20171221T133000 SUMMARY: Eelco Visser: Specification of Type Systems in Spoofax DESCRIPTION: The Spoofax language workbench supports the creation of progra mming environments for software languages using highlevel declarative meta languages for the various aspects of language definition. In this talk\, I will give a brief overview of the ...continue reading XALTDESC;FMTTYPE=text/html:The Spoofax language workbench supports th e creation of programming environments for software languages using highle vel declarative metalanguages for the various aspects of language definiti on. In this talk\, I will give a brief overview of the capabilities of Spoo fax and then zoom in on its metalanguage for the specification of type sys tems based on scope graphs for name binding and type constraints.
Lin
ks

http://www.metaborg.org
 A Theory of Name Resolution. ESOP 2016.
http://dx.doi.org/10.1007/9783662466698_9
 A cons
traint language for static semantic analysis based on scope graphs. PEPM 20
16. http://doi.acm.org/10.1145/2847538.2847543
In approximately 1993 Paul Klint and cowor kers developed the ATerm library as a basic library to perform language tra nsformations. The intention from the outside was that this library would be suitable for parallel processing\, but this never materialised. Throughout the years several experiment have been done and a number of quite advanced lock and wait free algorithms have been developed that are suitable to mak e the ATerm library parallel. We review some of these algorithms and the ex cessive time to develop them. With new standard language constructs in C++1 1 it is possible to make the ATerm library parallel and we report on the cu rrent state of affairs which as it stands is not yet convincing.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janfrisogrooteexperime ntswithaparallelatermlibrarythroughtheyears/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9998EO1121@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171207T090054Z LASTMODIFIED:20180122T154534Z DTSTART;TZID=Europe/Amsterdam:20171207T124500 DTEND;TZID=Europe/Amsterdam:20171207T133000 SUMMARY: Bas Luttik: A Kleene theorem for pomset languages DESCRIPTION: We take as starting point Kleene’s wellknown theorem establis hing a correspondence between regular expressions and finite automata: ever y language denoted by a regular expression is accepted by a finite automato n\, and every language accepted by ...continue reading XALTDESC;FMTTYPE=text/html:We take as starting point Kleene’s wellkn own theorem establishing a correspondence between regular expressions and f inite automata: every language denoted by a regular expression is accepted by a finite automaton\, and every language accepted by a finite automaton i s denoted by a regular expression. We extend regular expressions with a par allel construct and finite automata with a fork construction and establish a Kleene correspondence between the two in pomset language semantics.
This may be considered as a first step towards a Kleene theorem for Concur rent Kleene Algebra (CKA)\, an extension of Kleene Algebra with a parallel construct\, that was proposed by Hoare\, Möller\, Struth and Wehrman as a s uitable formal framework for the study of concurrent programs. CKA does req uire a different semantics satisfying the socalled exchange law between se quential and parallel composition.
The talk is based on joint work wi th Tobias Kappé\, Paul Brunet\, Alexandra Silva and Fabio Zanasi\, all from UCL.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/basluttikakleenetheor emforpomsetlanguages/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9934EO1381@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171130T090034Z LASTMODIFIED:20180708T174625Z DTSTART;TZID=Europe/Amsterdam:20171130T124500 DTEND;TZID=Europe/Amsterdam:20171130T133000 SUMMARY: Sander de Putter: Evaluation of compositional model checking DESCRIPTION: Although model checking is one of the most successful approach es for the analysis and verification of the behaviour of concurrent systems \, it is plagued with the socalled state space explosion problem\; the sta te space of ...continue reading XALTDESC;FMTTYPE=text/html:Although model checking is one of the most successful approaches for the analysis and verification of the behaviour o f concurrent systems\, it is plagued with the socalled state space explosi on problem\; the state space of a concurrent system tends to increase expon entially as the number of parallel processes increases linearly. To combat state space explosion several compositional verification approaches have be en proposed such as compositional aggregation and assumeguarantee reasonin g. In their evaluation of assume guarantee reasoning Cobleigh\, Avrunin\, a nd Clarke[1] rais doubts about the effectiveness of assumeguarantee reason ing. Inspired by this work\, my current work investigates the effectiveness of compositional aggregation. In contrast to [1]\, we also aim to characte rize situations when compositional aggregation is or is not effective. In t his talk I will briefly discuss [1] and present our methodology and prelimi nary results of our evaluation of compositional aggregation.
[1] Cobl eigh\, J.M.\, Avrunin\, G.S.\, Clarke\, L.A.: Breaking up is hard to do: An evaluation of automated assumeguarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2)\, 7:17:52(May 2008)
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/sanderdeputterevaluati onofcompositionalmodelchecking/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9871EO1461@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171120T090051Z LASTMODIFIED:20181031T192635Z DTSTART;TZID=Europe/Amsterdam:20171123T143000 DTEND;TZID=Europe/Amsterdam:20171123T153000 SUMMARY: Perry van Wesel: Formal analysis of ring networks DESCRIPTION: SystemsonChips rely on the correct functioning of the commun ication between their components. As these systems grow more complex\, so d o the underlying communication networks. Simulating a network does not guar antee the entire statespace is explored\, ...continue reading XALTDESC;FMTTYPE=text/html:SystemsonChips rely on the correct funct ioning of the communication between their components. As these systems grow more complex\, so do the underlying communication networks. Simulating a n etwork does not guarantee the entire statespace is explored\, therefore fo rmal verification methods should be used to ensure correctness of these Net worksonChips. This thesis uses the MaDL modelling language to model and v erify liveness of networks. Although MaDL is a useful tool for the verifica tion of networks\, it lacks the capability to completely model and analyse ring networks. Therefore\, MaDL is extended with a new primitive and a ring detection algorithm that cooperate to generate additional network invarian ts specifically for ring networks. These extensions are used in two case st udies to model and verify network architecture proposals from literature. T he analysed networks are TornadoNoC [10] and LIGERO [1]. In both case studi es\, the process of formally modelling these architectures reveals ambiguit y in the original proposal papers. Both architectures turn out to contain d eadlocks when modelling as close to their original proposal as possible. Th e results show formal modelling is a useful tool to eliminate ambiguity\, b ut still requires improvement to allow it to scale to larger networks. The extensions to MaDL prove to be useful when modelling certain networks\, but can still be improved to allow verification of a wider range of different networks.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 14 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/perryvanweselformalan alysisofringnetworks/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9798EO1421@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171123T090033Z LASTMODIFIED:20180708T174626Z DTSTART;TZID=Europe/Amsterdam:20171123T124500 DTEND;TZID=Europe/Amsterdam:20171123T133000 SUMMARY: Rodin Aarssen: Towards a generic framework for analyzing C++ in Ra scal DESCRIPTION: Maintenance of legacy software is often a costly task. Softwar e analysis tools can help a lot by providing insight in existing code. Howe ver\, for C++\, this tooling often doesn’t give satisfactory answers. In th is talk\, ...continue reading XALTDESC;FMTTYPE=text/html:Maintenance of legacy software is often a costly task. Software analysis tools can help a lot by providing insight in existing code. However\, for C++\, this tooling often doesn’t give satisfa ctory answers. In this talk\, I will introduce ClaiR\, a generic C++ analys is framework I built on top of the metaprogramming language Rascal. Also\, I will discuss its future directions and show a modeling result.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rodinaarssentowardsag enericframeworkforanalyzingcinrascal/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9739EO1451@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171119T090005Z LASTMODIFIED:20181031T192504Z DTSTART;TZID=Europe/Amsterdam:20171121T100000 DTEND;TZID=Europe/Amsterdam:20171121T110000 SUMMARY: Olav Bunte: Quantitative model checking on probabilistic systems u sing plmu*+ DESCRIPTION: Although most model checking logics focus on proving qualitati ve properties\, with the logic plmu*+ introduced in Mio’s PhD thesis one ca n check the probability that some behaviour happens. In this work we try to bring ...continue reading XALTDESC;FMTTYPE=text/html:Although most model checking logics focus on proving qualitative properties\, with the logic plmu*+ introduced in Mio 's PhD thesis one can check the probability that some behaviour happens. In this work we try to bring this logic to practice. We attempt to find intui tive meaning for plmu*+formulas with the aim to create guidelines to creat e meaningful formulas. Also\, we give an alternative representation of a pl mu*+ model checking problem in form of an equations system and we give an a lgorithm to extract the solution from this representation\, based on the wo rk of Mader. This algorithm will be compared to an approximation algorithm by applying both on a number of use cases.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 3 GEO:51.447567;5.487443 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/olavbuntequantitativem odelcheckingonprobabilisticsystemsusingplmu/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9669EO1431@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171116T090015Z LASTMODIFIED:20180708T174626Z DTSTART;TZID=Europe/Amsterdam:20171116T124500 DTEND;TZID=Europe/Amsterdam:20171116T133000 SUMMARY: Tim Willemse: Explorations of AttributeBased Access Control DESCRIPTION: AttributeBased Access Control (ABAC) is emerging as the de fa cto paradigm for the specification and enforcement of access control polici es. Nonetheless\, ABAC is vulnerable to attribute hiding attacks where user s can obtain a more favourable ...continue reading XALTDESC;FMTTYPE=text/html:AttributeBased Access Control (ABAC) is e merging as the de facto paradigm for the specification and enforcement of a ccess control policies. Nonetheless\, ABAC is vulnerable to attribute hidin g attacks where users can obtain a more favourable decision by hiding some of their attributes. The extended evaluation of an ABAC policy takes such a ttribute hiding into account and arguably allows to come to more precise de cisions. An extended evaluation of a given query is calculated using the ev aluation of all (sensible) queries that can be constructed from that query. Evidently\, this approach may require exploring the state space for all po ssible queries\; as such\, evaluating a query may not be particularly effic ient. In this talk we explore various techniques for computing the extended evaluation.
CATEGORIES:Colloquium LOCATION:MetaForum MF 6.131 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/timwillemseexplorations ofattributebasedaccesscontrol/ END:VEVENT BEGIN:VEVENT UID:20180105T1001Z1515146517.9567EO1441@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20190618T084143Z CREATED:20171102T090034Z LASTMODIFIED:20180708T174626Z DTSTART;TZID=Europe/Amsterdam:20171102T124500 DTEND;TZID=Europe/Amsterdam:20171102T133000 SUMMARY: Omar Alzuhaibi: Automata Learning in an Engineering Context DESCRIPTION: Implementing the theory of automata learning on practical syst ems comes with many challenges\, more so when learning legacy systems. In t his talk\, I will present some of the challenges I faced while learning a l egacy ...continue reading XALTDESC;FMTTYPE=text/html:Implementing the theory of automata learni ng on practical systems comes with many challenges\, more so when learning legacy systems. In this talk\, I will present some of the challenges I face d while learning a legacy component in an industrial setting at Philips Hea lthcare\, how I managed to overcome some of those challenges\, and how I pl an to solve the rest. Such challenges range from initially setting up the l earning environment to dealing with asynchronous calls and parallelism to s calability and efficiency.
CATEGORIES:Colloquium LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/omaralzuhaibiautomatal earninginanengineeringcontext/ END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Amsterdam BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 DTSTART:20171029T010000 TZNAME:CET END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 DTSTART:20180325T010000 TZNAME:CEST END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 DTSTART:20181028T010000 TZNAME:CET END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 DTSTART:20190331T010000 TZNAME:CEST END:DAYLIGHT END:VTIMEZONE END:VCALENDAR