In this talk\, I will discuss McMillan's a lgorithm for fully SATbased unbounded symbolic model checking. The method is based on computing Craig interpolants. In terms of performance\, the alg orithm is substantially more efficient than BDDbased model checking. I wil l also explain how we modify McMillan's algorithm to analyze the backward r eachability of initial states from final states in a transition system.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/alexanderfedotovmcmilla nsalgorithmforsatbasedunboundedmodelchecking/ END:VEVENT BEGIN:VEVENT UID:20210428T0944Z1619603045.5809EO8931@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210428T094236Z LASTMODIFIED:20210428T094236Z DTSTART;TZID=Europe/Amsterdam:20210429T124500 DTEND;TZID=Europe/Amsterdam:20210429T133000 SUMMARY: Flip van Spaendonck: Understanding std::memory_order in C++11 usin g MCA semantics DESCRIPTION: C++11 introduced many tools to write safe multi threaded code. One of those tools are the std::memory_orders\, which specify how memory a ccesses\, including regular\, nonatomic memory accesses\, are to be ordere d around atomic operations. Understanding these memory orders can be quite a complex situation\, specifically when different memory orders are combine d. We will try to make ...continue reading XALTDESC;FMTTYPE=text/html:C++11 introduced many tools to write safe multi threaded code. One of those tools are the std::memory_orders\, which specify how memory accesses\, including regular\, nonatomic memory accesse s\, are to be ordered around atomic operations. Understanding these memory orders can be quite a complex situation\, specifically when different memor y orders are combined. We will try to make sense of these by using mCRL2 to analyze all traces possible under MCA semantics. A set of semantics in whi ch all threads perceive memory accesses in the same order.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/flipvanspaendonckunder standingstdmemory_orderinc11usingmcasemantics/ END:VEVENT BEGIN:VEVENT UID:20210421T0838Z1618994304.8504EO8901@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210421T081344Z LASTMODIFIED:20210421T081344Z DTSTART;TZID=Europe/Amsterdam:20210422T150000 DTEND;TZID=Europe/Amsterdam:20210422T154500 SUMMARY: Geert van Ieperen: Visualisation of large Labelled Transition Syst ems DESCRIPTION: A formal model describes the behaviour of a program\, protocol or other system. The properties of this model can be verified\, such that we can prove these properties with absolute certainty. Visualising the stat e space of a formal model is an important tool for their development. This thesis focuses on visualising such a state space ...continue reading XALTDESC;FMTTYPE=text/html:A formal model describes the behaviour of
a program\, protocol or other system. The properties of this model can be v
erified\, such that we can prove these properties with absolute certainty.
Visualising the state space of a formal model is an important tool for thei
r development. This thesis focuses on visualising such a state space as a g
raph.
We present a layout technique that provides efficient graph layo
uts for graphs with over 10000 nodes\, discuss the effectiveness of differe
nt edge shapes\, and present multiple ways of highlighting the structure of
the graph. We present a rendering procedure capable of rendering graphs la
rger than 10000 nodes while supporting these techniques. We implemented the
se techniques in a tool and use it to measure the performance of the techni
ques. The effectiveness of these techniques is analysed using a survey on t
he tool in a few practical applications.
We conclude that these techn iques can effectively be used in one visualisation to assist in formal mode l development.
The tool is registered on DOI 10.5281/zenodo.4680646 CATEGORIES:MSc Defence LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Tim Willemse":MAILTO:t.a.c.willemse@gmail.com URL;VALUE=URI:https://fsa.win.tue.nl/events/event/geertvanieperenvisuali sationoflargelabelledtransitionsystems/ END:VEVENT BEGIN:VEVENT UID:20210421T0626Z1618986404.2484EO8871@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210421T055419Z LASTMODIFIED:20210421T055419Z DTSTART;TZID=Europe/Amsterdam:20210422T124500 DTEND;TZID=Europe/Amsterdam:20210422T133000 SUMMARY: Anna Stramaglia: Deadlock in packet switching networks DESCRIPTION: A deadlock in a packet switching network is a state in which o ne or more messages have not yet reached their target\, yet cannot progress any further. We formalize three different notions of deadlock in the conte xt of packet switching networks\, to which we refer as global\, local and w eak deadlock. We establish the precise ...continue reading XALTDESC;FMTTYPE=text/html:
A deadlock in a packet switching network i s a state in which one or more messages have not yet reached their target\, yet cannot progress any further. We formalize three different notions of d eadlock in the context of packet switching networks\, to which we refer as global\, local and weak deadlock. We establish the precise relations betwee n these notions\, and prove they characterize different sets of deadlocks. Moreover\, we implement checking of deadlock freedom of packet switching ne tworks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in pa cket switching networks.
This is joint work with Jeroen J.A. Keiren a nd Hans Zantema
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/annastramagliadeadlock inpacketswitchingnetworks2/ END:VEVENT BEGIN:VEVENT UID:20210414T1814Z1618424068.1355EO8831@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210414T172217Z LASTMODIFIED:20210414T172217Z DTSTART;TZID=Europe/Amsterdam:20210415T124500 DTEND;TZID=Europe/Amsterdam:20210415T133000 SUMMARY: Muhammad Osama: SAT Solving with GPU Accelerated Inprocessing DESCRIPTION: Since 2013\, the leading SAT solvers in the SAT competition al l use inprocessing\, which unlike preprocessing\, interleaves search with s implifications. However\, applying inprocessing frequently can still be a b ottle neck\, i.e.\, for hard or large formulas. In this work\, we introduce the first attempt to parallelize inprocessing on GPU architectures. As mem ory is a scarce ...continue reading XALTDESC;FMTTYPE=text/html:Since 2013\, the leading SAT solvers in th e SAT competition all use inprocessing\, which unlike preprocessing\, inter leaves search with simplifications. However\, applying inprocessing frequen tly can still be a bottle neck\, i.e.\, for hard or large formulas. In this work\, we introduce the first attempt to parallelize inprocessing on GPU a rchitectures. As memory is a scarce resource in GPUs\, we present new space efficient data structures and devise a dataparallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memo ry access locality. Our new parallel variable elimination algorithm is twic e as fast as previous work. In experiments our new solver ParaFROST solves many benchmarks faster on the GPU than its sequential counterparts.
T his is a joint work with Armin Biere (Johannes Kepler University).
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/muhammadosamasatsolvin gwithgpuacceleratedinprocessing/ END:VEVENT BEGIN:VEVENT UID:20210406T1604Z1617725083.7118EO8821@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210406T160114Z LASTMODIFIED:20210406T160114Z DTSTART;TZID=Europe/Amsterdam:20210408T124500 DTEND;TZID=Europe/Amsterdam:20210408T133000 SUMMARY: Rick Erkens: A Set Automaton to Locate All Pattern Matches in a Te rm DESCRIPTION: Term pattern matching is the problem of finding all pattern ma tches in a subject term\, given a set of patterns. It is a fundamental algo rithmic problem in for instance automated theorem proving and term rewritin g. We present a set automaton solution for the term pattern matching proble m that is based on match set derivatives where ...continue reading XALTDESC;FMTTYPE=text/html:Term pattern matching is the problem of fi nding all pattern matches in a subject term\, given a set of patterns. It i s a fundamental algorithmic problem in for instance automated theorem provi ng and term rewriting. We present a set automaton solution for the term pat tern matching problem that is based on match set derivatives where each fun ction symbol in the subject pattern is visited exactly once. The algorithm allows for various traversal patterns over the subject term and is particul arly suited to search the subject term in parallel using a large number of simultaneously running threads.
This is joint work with Jan Friso Gro ote.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rickerkensasetautomat ontolocateallpatternmatchesinaterm/ END:VEVENT BEGIN:VEVENT UID:20210401T1030Z1617273054.9847EO8681@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210401T100503Z LASTMODIFIED:20210401T100503Z DTSTART;TZID=Europe/Amsterdam:20210401T124500 DTEND;TZID=Europe/Amsterdam:20210401T133000 SUMMARY: Bas Luttik: Equationally axiomatising parallel composition DESCRIPTION: I will overview some results pertaining to the (equational) ax iomatisation of interleaving parallel composition. XALTDESC;FMTTYPE=text/html:I will overview some results pertaining to the (equational) axiomatisation of interleaving parallel composition.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/basluttikequationallya xiomatisingparallelcomposition/ END:VEVENT BEGIN:VEVENT UID:20210323T1401Z1616508077.175EO8661@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210323T135413Z LASTMODIFIED:20210323T135413Z DTSTART;TZID=Europe/Amsterdam:20210325T124500 DTEND;TZID=Europe/Amsterdam:20210325T133000 SUMMARY: Jan Friso Groote: Partition refinement algorithms for strong bisim ulation are Omega(n log n) DESCRIPTION: A question haunting me for a while is whether the O(m log n) a lgorithm for strong bisimulation is optimal. We found a family of graphs th at shows that any reasonable partition refinement algorithm is necessarily Omega(n log n)\, n being the number of states\, steps to calculate strong bisimulation. This appeared to answer the question. ...continue reading XALTDESC;FMTTYPE=text/html:A question haunting me for a while is whet her the O(m log n) algorithm for strong bisimulation is optimal. We found a family of graphs that shows that any reasonable partition refinement algo rithm is necessarily Omega(n log n)\, n being the number of states\, steps to calculate strong bisimulation. This appeared to answer the question. Bu t some results from the literature  digged up by Jan Martens  puts our finding in a strange light. There is a family of graphs for which branchin g bisimulation can be calculated linearly\, but which still is Omega(n log n) when partition refinement is applied. These results need to be understoo d further\, but in extremo this suggests that partition refinement is not s uch a good idea after all.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janfrisogrootepartitio nrefinementalgorithmsforstrongbisimulationareomeganlogn/ END:VEVENT BEGIN:VEVENT UID:20210316T1334Z1615901655.9545EO8651@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210316T131937Z LASTMODIFIED:20210316T131937Z DTSTART;TZID=Europe/Amsterdam:20210318T124500 DTEND;TZID=Europe/Amsterdam:20210318T133000 SUMMARY: Hans Zantema: Complexity of Simon’s problem in classical sense DESCRIPTION: Simon’s problem is a standard example of a problem that is exp onential in classical sense\, while it admits a linear solution in quantum computing. It is about a function f for which it is given that a unique non zero vector s exists for which f(x) = f(x xor s) for all x. The goal is to find s. The ...continue reading XALTDESC;FMTTYPE=text/html:Simon's problem is a standard example of a problem that is exponential in classical sense\, while it admits a linear solution in quantum computing. It is about a function f for which it is giv en that a unique nonzero vector s exists for which f(x) = f(x xor s) for a ll x. The goal is to find s. The exponential lower bound for the classical sense assumes that f only admits black box access. In this presentation we investigate classical complexity when f is given by a standard representati on like a circuit. We focus on finding the vector space of all vectors s fo r which f(x) = f(x xor s) for all x\, for any given f. Two main results are : (1) if f is given by any circuit\, then checking whether this vector spac e contains a nonzero element is NPhard\, and (2) when restricting to BDDs \, then a basis of this vector space can be computed in polynomial time.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hanszantemacomplexityo fsimonsprobleminclassicalsense/ END:VEVENT BEGIN:VEVENT UID:20210309T2106Z1615324017.97EO8621@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210309T203356Z LASTMODIFIED:20210309T203356Z DTSTART;TZID=Europe/Amsterdam:20210311T124500 DTEND;TZID=Europe/Amsterdam:20210311T133000 SUMMARY: Jan Martens: Solving bisimilarity and the relational coarsest part ition problem in sublinear parallel time seems hard DESCRIPTION: It is known that deciding bisimilarity is a Pcomplete problem . This means it is thought of as a problem that is inherently sequential an d hard to solve in parallel. Despite this fact efforts have been made to co nstruct increasingly efficient parallel algorithms. In a previous colloquiu m I presented a parallel algorithm that decides bisimilarity in ...continue reading XALTDESC;FMTTYPE=text/html:It is known that deciding bisimilarity is a Pcomplete problem. This means it is thought of as a problem that is inhe rently sequential and hard to solve in parallel. Despite this fact efforts have been made to construct increasingly efficient parallel algorithms. In a previous colloquium I presented a parallel algorithm that decides bisimil arity in O(n) time on n+m parallel processors that are allowed to concurren tly read and write. In this talk I will discuss what the parallel intractab ility of Pcomplete problems means\, and what this means for further improv ements of the algorithm.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janmartenssolvingbisim ilarityandtherelationalcoarsestpartitionprobleminsublinearparalle ltimeseemshard/ END:VEVENT BEGIN:VEVENT UID:20210302T0924Z1614677043.9817EO8581@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210302T090624Z LASTMODIFIED:20210302T090624Z DTSTART;TZID=Europe/Amsterdam:20210304T124500 DTEND;TZID=Europe/Amsterdam:20210304T133000 SUMMARY: Erik de Vink: On Quantum Process Algebra DESCRIPTION: After a quick intro to quantum computing addressing Deutsch’s problem\, we turn to quantum teleportation and look into what may be needed to handle such with a tool like (probabilistic) mCRL2. XALTDESC;FMTTYPE=text/html:After a quick intro to quantum computing a ddressing Deutsch's problem\, we turn to quantum teleportation and look int o what may be needed to handle such with a tool like (probabilistic) mCRL2.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/erikdevinkonquantump rocessalgebra/ END:VEVENT BEGIN:VEVENT UID:20210222T1459Z1614005974.4316EO8571@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210222T140535Z LASTMODIFIED:20210222T140535Z DTSTART;TZID=Europe/Amsterdam:20210225T124500 DTEND;TZID=Europe/Amsterdam:20210225T133000 SUMMARY: Maurice Laveaux: Antichain Based Algorithm for Fair Testing DESCRIPTION: The notion of refinement plays an important role in software e ngineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving\, or computing\, that a system refines its specification. There are many refinement relation s described in the literature. Fair testing is the coarsest livenesspreser ving ...continue reading XALTDESC;FMTTYPE=text/html:The notion of refinement plays an importan t role in software engineering. It is the basis of a stepwise development m ethodology in which the correctness of a system can be established by provi ng\, or computing\, that a system refines its specification. There are many refinement relations described in the literature. Fair testing is the coar sest livenesspreserving refinement relation that is a precongruence for a CSP inspired process algebra. The main feature of fair testing is that it a bstracts from divergences in the same way as Milner's observation congruenc e\, and as a result is also strictly coarser than observation congruence. T his can be seen as a builtin fairness assumption. Fair testing has been sh own to be decidable\, but its algorithm is not yet practical. In this prese ntation I will describe fair testing and the algorithm. Furthermore\, I wil l also explain the applicability of antichains to improve the efficiency of the algorithm.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mauricelaveauxantichain basedalgorithmforfairtesting/ END:VEVENT BEGIN:VEVENT UID:20210208T0837Z1612773463.0867EO8561@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210208T080235Z LASTMODIFIED:20210208T080235Z DTSTART;TZID=Europe/Amsterdam:20210211T124500 DTEND;TZID=Europe/Amsterdam:20210211T133000 SUMMARY: Ferry Timmers: Statespace exploration of generated system control lers DESCRIPTION: Modeldriven system engineering is a practice also employed in the design of controllers for cyberphysical systems. The method allows co ntrollers to be modelled and verified before they are implemented in softwa re\, allowing potential glitches and design flaws to be uncovered\, before they emerge in the time and resource intensive testing phase. Some of the m odelling ...continue reading XALTDESC;FMTTYPE=text/html:Modeldriven system engineering is a pract ice also employed in the design of controllers for cyberphysical systems. The method allows controllers to be modelled and verified before they are i mplemented in software\, allowing potential glitches and design flaws to be uncovered\, before they emerge in the time and resource intensive testing phase. Some of the modelling formalisms used by the industry allow controll ers to be automatically generated from models\, which aides in the preventi on of human error in the implementation of such systems. The question arise s whether the behavior of the generated software components is equivalent t o those of the specified models\, as the semantics of such systems might no t always be trivially deduced. The topic of this talk is about how to solve this problem. It will present a way to deduct the statespace from impleme nted software controllers\, and the intricacies of this approach. It will g ive the context of where this question arose\, and what its contribution ca n potentially be for the industry and in a general setting. It will conclud e with a few examples to shows the approach in working order\, and if you a re still reading this\, given there is enough time and interest in the subj ect a more interactive demonstration.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ferrytimmersstatespace explorationofgeneratedsystemcontrollers/ END:VEVENT BEGIN:VEVENT UID:20210201T1201Z1612180908.5806EO8551@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210201T113516Z LASTMODIFIED:20210201T113516Z DTSTART;TZID=Europe/Amsterdam:20210204T124500 DTEND;TZID=Europe/Amsterdam:20210204T133000 SUMMARY: Yousra Hafidi: Modeling and Improved Verification of Reconfigurabl e Discrete Event Systems using RTNCESs Formalism DESCRIPTION: Reconfigurability is a concept that appeared recently in sever al areas including manufacturing\, aerospace\, medical\, robotic\, and tele communication systems. This concept provides systems with an aspect of flex ibility allowing them to easily adapt with their external environment durin g their working process. Reconfiguration provides many advantages to variou s existing systems. However\, by adopting such aspect\, some issues ...cont inue reading XALTDESC;FMTTYPE=text/html:Reconfigurability is a concept that appear ed recently in several areas including manufacturing\, aerospace\, medical\ , robotic\, and telecommunication systems. This concept provides systems wi th an aspect of flexibility allowing them to easily adapt with their extern al environment during their working process.
Reconfiguration provides many advantages to various existing systems. However\, by adopting such as pect\, some issues can be confronted and deserve to be resolved. In this ta lk we will treat problems related to the modeling and the verification of r econfigurable systems using reconfigurable timed net condition/event system s (RTNCES) formalism. RTNCESs formalism is a modular extension of Petri n ets enriched with conditions\, events\, time\, and reconfiguration constrai nts.
This work was part of my PhD research works in collaboration wit h University of Tunis El Manar\, Jinan University\, and University of Moham ed Khider Biskra.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/yousrahafidimodelingan dimprovedverificationofreconfigurablediscreteeventsystemsusingrtn cessformalism/ END:VEVENT BEGIN:VEVENT UID:20210127T0905Z1611738336.9966EO8541@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210127T084714Z LASTMODIFIED:20210128T074133Z DTSTART;TZID=Europe/Amsterdam:20210128T124500 DTEND;TZID=Europe/Amsterdam:20210128T133000 SUMMARY: Jeroen Keiren: Peterson’s mutual exclusion algorithm for n process es DESCRIPTION: When talking about mutual exclusion\, many textbooks start by introducing Peterson’s algorithm for two processes. The algorithm looks ver y simple\, but upon closer inspection its behaviour is deceptively subtle. Less commonly known are extensions of Peterson’s algorithm to n processes. In this talk\, I will look at such generalisations. I will also describe ho w these ...continue reading XALTDESC;FMTTYPE=text/html:When talking about mutual exclusion\, many textbooks start by introducing Peterson’s algorithm for two processes. The algorithm looks very simple\, but upon closer inspection its behaviour is deceptively subtle. Less commonly known are extensions of Peterson’s algori thm to n processes. In this talk\, I will look at such generalisations. I w ill also describe how these processes can be modelled and verified using mC RL2.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/jeroenkeirenpetersonsm utualexclusionalgorithmfornprocesses/ END:VEVENT BEGIN:VEVENT UID:20210120T1007Z1611137276.958EO8531@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210120T083413Z LASTMODIFIED:20210120T083413Z DTSTART;TZID=Europe/Amsterdam:20210121T124500 DTEND;TZID=Europe/Amsterdam:20210121T133000 SUMMARY: Mark Bouwman: Direct formalization of EULYNX SysML in mCRL2 DESCRIPTION: FormaSig aims to strengthen railway signalling standardization processes with the use of formal methods. The concrete approach investigat ed in FormaSig is to derive formal mCRL2 models from existing SysML specifi cations. These formal models are then used for two distinct purposes: (i) c hecking whether the original standard satisfies the requirements that are i mposed upon them\, and ...continue reading XALTDESC;FMTTYPE=text/html:FormaSig aims to strengthen railway signal ling standardization processes with the use of formal methods. The concrete approach investigated in FormaSig is to derive formal mCRL2 models from ex isting SysML specifications. These formal models are then used for two dist inct purposes: (i) checking whether the original standard satisfies the req uirements that are imposed upon them\, and (ii) performing automated testin g of implementations. In this talk I will present our approach to developin g a translation from SysML to mCRL2. We define the semantics of state machi nes directly in mCRL2. The model containing the generic semantics then only needs to be completed with a specific instantiation of state machines by e ncoding the structure of these state machines in the mCRL2 data language. W e have a prototype translation tool that takes a number of SysML diagrams a nd produces such a configuration.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/markbouwmandirectforma lizationofeulynxsysmlinmcrl2/ END:VEVENT BEGIN:VEVENT UID:20210104T1500Z1609772418.1938EO8451@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20210104T145819Z LASTMODIFIED:20210104T145819Z DTSTART;TZID=Europe/Amsterdam:20210107T124500 DTEND;TZID=Europe/Amsterdam:20210107T133000 SUMMARY: Wieger Wesselink: Symbolic Reachability using LDDs DESCRIPTION: The mCRL2 toolset contains several applications in which compu ting the set of reachable states of a transition relation plays a role. For example in state space generation and in solving a PBES. List decision dia grams (LDDs) can be used to store sets of states and transitions in a compa ct manner. This has been demonstrated by ...continue reading XALTDESC;FMTTYPE=text/html:The mCRL2 toolset contains several applica tions in which computing the set of reachable states of a transition relati on plays a role. For example in state space generation and in solving a PBE S. List decision diagrams (LDDs) can be used to store sets of states and tr ansitions in a compact manner. This has been demonstrated by Jaco van de Po l and Stefan Blom in 2008\, and these ideas have been implemented in the LT SMin toolset. We are currently applying these ideas in the mCRL2 toolset as well\, using the LDD functionality of the Sylvan library made by Tom van D ijk. In this talk I will explain the main ideas behind it\, and describe a reachability algorithm that uses LDDs.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/wiegerwesselinksymbolic reachabilityusingldds/ END:VEVENT BEGIN:VEVENT UID:20201214T2337Z1607989074.2596EO8431@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201214T210526Z LASTMODIFIED:20201214T213157Z DTSTART;TZID=Europe/Amsterdam:20201217T124500 DTEND;TZID=Europe/Amsterdam:20201217T133000 SUMMARY: Herman Geuvers: Relating Apartness and Bisimulation DESCRIPTION: We have studied the dual of bisimulation: the notion of “apart ness”. Intuitively\, two elements are apart if there is a positive way to d istinguish them. Apartness is the dual of bisimilarity in a precise categor ical sense: apartness is an initial algebra and gives rise to an induction principle. In the talk we will focus on the inductive nature of ...continue reading XALTDESC;FMTTYPE=text/html:We take a look at kDFAOs\, which are Dete
rministic Finite Automata with Output with a special property: each kDFAO
represents a kautomatic sequence a\, an infinite sequence in which the it
h element is the output the automata produces for the kary representation
of i. Given any kautomatic sequence a\, we define their complexity ak
as the size of the smallest possible kDFAO representing our sequence and s
imilarly the reverse complexity aRk for the right to left representatio
n of kary numbers.
To be more specific\, we look at local changes f t
o our sequences\, that only change a finite amount of elements\, and find a
n upper bound for the complexities f(a)k and f(a)Rk\, when applied
to an arbitrary sequence a.
We then use SAT/SMT solvers to prove that
these upper bounds can not be further improved\, thus establishing a lower
bound as well.
We also create an algorithm for minimizing any kDFAO\,
which will give us a more efficient way of getting ak than using a SAT
/SMT solver.
Whenever two Labelled Transition Systems ( LTSs) are behaviourally inequivalent to each other\, one may be interested why this is the case. Using a modal logic that characterises such a behavio ural equivalence one can create formulae that distinguish these two LTSs\, exposing the reason for the inequivalence. In this presentation I will desc ribe the work by Rance Cleaveland on computing distinguishing formulae for strong bisimulation and the work by Henri Korver on computing distinguishin g formulae for branching bisimulation. Also\, I will compare the work of Ko rver with an alternate logic for characterising branching bisimulation and propose ideas to (possibly) improve on Korvers work.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/olavbunteevidenceforb ehaviouralinequivalence/ END:VEVENT BEGIN:VEVENT UID:20201123T1055Z1606128910.1675EO8371@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201123T104809Z LASTMODIFIED:20201123T104809Z DTSTART;TZID=Europe/Amsterdam:20201127T130000 DTEND;TZID=Europe/Amsterdam:20201127T134500 SUMMARY: Wouter Schols: Verification of an iterative implementation of Tarj an’s algorithm for Strongly Connected Components using Dafny DESCRIPTION: Tarjan’s algorithm for strongly connected components is used i n the mCRL2 toolset. This algorithm finds all strongly connected components or SCC in a directed graph. Here an SCC is a maximal set of nodes such tha t there exists a directed path between all nodes in the set. The normal imp lementation of Tarjan’s algorithm uses recursion. ...continue reading XALTDESC;FMTTYPE=text/html:Tarjan’s algorithm for strongly connected components is used in the mCRL2 toolset. This algorithm finds all strongly connected components or SCC in a directed graph. Here an SCC is a maximal s et of nodes such that there exists a directed path between all nodes in the set. The normal implementation of Tarjan’s algorithm uses recursion. Unfor tunately\, this implementation can cause stack overflow problems if the gra phs are sufficiently large. The mCRL2 toolset uses an iterative implementat ion of Tarjan’s algorithm to circumvent this problem. In this project both the recursive and the much more complex iterative algorithm have been prove n correct using the verification language Dafny. For the recursive algorith m a previous proof was already available. However this proof was nearing th e limits of Dafny’s capabilities\, which caused unstable results after mino r changes. As part of this work techniques have been introduced to guarante e much more stable proofs.
CATEGORIES:MSc Defence LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Wieger Wesselink":MAILTO:J.W.Wesselink@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/wouterscholsverificatio nofaniterativeimplementationoftarjansalgorithmforstronglyconnecte dcomponentsusingdafny/ END:VEVENT BEGIN:VEVENT UID:20201123T2049Z1606164582.8019EO8381@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201123T182733Z LASTMODIFIED:20201123T182821Z DTSTART;TZID=Europe/Amsterdam:20201126T124500 DTEND;TZID=Europe/Amsterdam:20201126T133000 SUMMARY: Anton Wijs: “Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion” DESCRIPTION: When targeting modern parallel hardware architectures\, constr ucting correct and highperforming software is complex and timeconsuming. In particular\, reorderings of memory accesses that violate intended sequen tially consistent behaviour are a major source of bugs. Applying synchronis ation mechanisms to repair these should be done sparingly\, as they negativ ely impact performance. In the past\, both static analysis approaches and t echniques ...continue reading XALTDESC;FMTTYPE=text/html: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 the past\, both static
analysis approaches and techniques based on explicitstate model checking
have been proposed to identify where synchronisation fences have to be plac
ed in a program. The former are fast\, but the latter more precise\, as the
y tend to insert fewer fences. Unfortunately\, the model checking technique
s suffer a form of state space explosion that is even worse than the
t
raditional one.
In this work\, we propose a technique using a combina tion of state space exploration and static analysis. This combination is in terms of precision comparable to purely model checkingbased techniques\, but it reduces the state space explosion problem to the one typically seen in model checking. Furthermore\, experiments show that the combination freq uently outperforms both purely model checking and static analysis technique s. In addition\, we have added the capability to check for atomicity violat ions\, which is another major source of bugs.
I have talked about thi s topic before in the FSA colloquium\, but since then\, this work has been accepted\, and presented last week\, at iFM 2020. Since the previous talk\, a new implementation of the approach has been constructed\, and new experi ments have been performed\, providing interesting insights.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/antonwijslockandfence whenneededstatespaceexplorationstaticanalysisimprovedfenceandloc kinsertion/ END:VEVENT BEGIN:VEVENT UID:20201118T0828Z1605688091.6695EO8201@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201118T082605Z LASTMODIFIED:20201118T082605Z DTSTART;TZID=Europe/Amsterdam:20201119T124500 DTEND;TZID=Europe/Amsterdam:20201119T133000 SUMMARY: Tim Willemse: On Recursive Algorithms for Solving Parity Games DESCRIPTION: Parity Games are infinite duration\, twoplayer graph games. S uch games play an important role in verification\, satisfiability and synth esis. In recent years\, several quasipolynomial time algorithms for solvin g parity games have appeared. One of the more recent ones\, by Pawel Parys\ , is based on the classical divideandconquer algorithm by McNaughton/Ziel onka. In this talk\, I will ...continue reading XALTDESC;FMTTYPE=text/html:Parity Games are infinite duration\, twop layer graph games. Such games play an important role in verification\, sati sfiability and synthesis. In recent years\, several quasipolynomial time a lgorithms for solving parity games have appeared. One of the more recent on es\, by Pawel Parys\, is based on the classical divideandconquer algorith m by McNaughton/Zielonka. In this talk\, I will reiterate this classical al gorithm and shed some light on the modifications that allow for achieving t he quasipolynomial runtime. While the big leap in runtime complexity is im pressive\, experiments indicate that the performance of this new algorithm sucks. This seems to be characteristic for all 'improved' algorithms.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/timwillemseonrecursive algorithmsforsolvingparitygames/ END:VEVENT BEGIN:VEVENT UID:20201109T1542Z1604936552.185EO8181@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201109T133936Z LASTMODIFIED:20201109T133936Z DTSTART;TZID=Europe/Amsterdam:20201112T124500 DTEND;TZID=Europe/Amsterdam:20201112T133000 SUMMARY: Rick Erkens: “Bloom’s Cool Congruence Formats for Weak Behavioral Equivalences: Make Branching Bisimilarity a Congruence Again” DESCRIPTION: The field of process algebra provides a way to model (concurre nt) processes algebraically. The syntax of a process calculus is described by an algebraic signature and the semantics is described by a set of operat ional rules. Strong bisimilarity and branching bisimilarity are two well kn own behavioral equivalences on processes. Informally two processes are stro ngly bisimilar ...continue reading XALTDESC;FMTTYPE=text/html:The field of process algebra provides a wa y to model (concurrent) processes algebraically. The syntax of a process ca lculus is described by an algebraic signature and the semantics is describe d by a set of operational rules. Strong bisimilarity and branching bisimila rity are two well known behavioral equivalences on processes. Informally tw o processes are strongly bisimilar if they cannot be distinguished by an ex ternal observer. Branching bisimilarity is a weaker equivalence that abstra cts from internal transitions.
In many process calculi\, strong bisim ilarity is a congruence. Informally this enables one to reason algebraicall y about strong bisimilarity of two processes. The GSOS format is a family o f process calculi for which strong bisimilarity is guaranteed to be a congr uence. Unfortunately branching bisimilarity is not a congruence for a GSOS language in general. To mitigate this issue\, Bard Bloom introduced languag e formats by putting extra restrictions on the GSOS rules. In particular th e BBcool format guarantees that branching bisimilarity is a congruence.
In this talk I will demonstrate why congruence is a complicated issue i n weak behavioral equivalences. We will discuss the GSOS format\, the BBco ol format\, and a sketch of a proof by Rob van Glabbeek that shows why the restrictions on GSOS are enough to make branching bisimilarity a congruence again. Currently I am studying this topic at a more abstract level with Ba s Luttik and Jurriaan Rot\, which I will briefly comment on.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rickerkensbloomscoolc ongruenceformatsforweakbehavioralequivalencesmakebranchingbisimilar ityacongruenceagain/ END:VEVENT BEGIN:VEVENT UID:20201103T1323Z1604409790.0398EO8171@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201103T121939Z LASTMODIFIED:20201103T121939Z DTSTART;TZID=Europe/Amsterdam:20201105T124500 DTEND;TZID=Europe/Amsterdam:20201105T133000 SUMMARY: Maurice Laveaux: Decompositional Minimisation of Monolithic Proces ses DESCRIPTION: Compositional minimisation can be an effective technique to re duce the state space explosion problem. This technique considers a parallel composition of several processes. In its simplest form\, each sequential p rocess is replaced by an abstraction\, simpler than the corresponding proce ss while still preserving the property that is checked. However\, this tech nique cannot be applied in ...continue reading XALTDESC;FMTTYPE=text/html:Compositional minimisation can be an effec tive technique to reduce the state space explosion problem. This technique considers a parallel composition of several processes. In its simplest form \, each sequential process is replaced by an abstraction\, simpler than the corresponding process while still preserving the property that is checked. However\, this technique cannot be applied in a setting where parallel com position is first translated to a nondeterministic sequential monolithic p rocess. The advantage of this monolithic process is that it facilitates sta tic analysis of global behaviour. We present a technique that considers a m onolithic process with data and decomposes it into two processes where each process defines behaviour for a subset of the parameters of the monolithic process. In this talk I will also highlight some of the practical consider ations of this technique and the results that have been achieved sofar.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mauricelaveauxdecomposi tionalminimisationofmonolithicprocesses/ END:VEVENT BEGIN:VEVENT UID:20201026T1634Z1603730050.347EO8151@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201026T150407Z LASTMODIFIED:20201026T150407Z DTSTART;TZID=Europe/Amsterdam:20201029T124500 DTEND;TZID=Europe/Amsterdam:20201029T133000 SUMMARY: Bas Luttik: Offtheshelf automated analysis of liveness propertie s for just paths DESCRIPTION: The motivation for the research that I will discuss in my talk is a claim by van Glabbeek and Höfner that CCSlike process algebras are n ot powerful enough to establish correctness of Peterson’s algorithm\, and\, in particular\, prove the required liveness property. The culprit\, accord ing to van Glabbeek and Höfner\, is that for these process ...continue read ing XALTDESC;FMTTYPE=text/html:Bram Hooimeijer did do his research for th e master thesis at ASML. The question was whether it is possible to constru ct models for the behaviour of software out of a single trace using informa tion about the software architecture. Bram showed that it was possible to c ome up with a reasonable model that could even be finetuned by analysing th e obtained model\, for instance for deadlocks and by adding meta informatio n to the model for instance about the allowed ordering of certain events in the software.
CATEGORIES:MSc Defence LOCATION:MS Teams 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/bramhooimeijermodelinf erenceforlegacysoftwareincomponentbasedarchitectures/ END:VEVENT BEGIN:VEVENT UID:20201012T1431Z1602513063.2887EO8041@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201012T141507Z LASTMODIFIED:20201012T141507Z DTSTART;TZID=Europe/Amsterdam:20201015T124500 DTEND;TZID=Europe/Amsterdam:20201015T133000 SUMMARY: Hans Zantema: Complexity of puzzles DESCRIPTION: For several puzzles (often from Japanese origin) the following can be investigated How to solve them\, either by backtracking or by SAT/S MT? How to generate them? How to prove NPcompleteness? Currently I supervi se several students in Nijmegen doing projects in this area. In this talk t hese projects will be discussed. XALTDESC;FMTTYPE=text/html:For several puzzles (often from Japanese o rigin) the following can be investigated
Currently I supervise several stude nts in Nijmegen doing projects in this area. In this talk these projects wi ll be discussed.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hanszantemacomplexityo fpuzzles/ END:VEVENT BEGIN:VEVENT UID:20201006T1718Z1602004688.1285EO8011@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20201006T170020Z LASTMODIFIED:20201006T170020Z DTSTART;TZID=Europe/Amsterdam:20201008T124500 DTEND;TZID=Europe/Amsterdam:20201008T133000 SUMMARY: Jan Martens: A parallel algorithm for bisimulation partition refin ement DESCRIPTION: The notion of strong bisimilarity on LTSs is an equivalence th at expresses whether states have the same behavior. In their pioneering wor k Kanellakis and Smolka proposed a partition refinement algorithm that find s the coarsest partition of bisimilar states. We propose a parallel version of this algorithm that performs this partition refinement on an LTS with . ..continue reading XALTDESC;FMTTYPE=text/html:The notion of strong bisimilarity on LTSs is an equivalence that expresses whether states have the same behavior. In their pioneering work Kanellakis and Smolka proposed a partition refinement algorithm that finds the coarsest partition of bisimilar states. We propos e a parallel version of this algorithm that performs this partition refinem ent on an LTS with n states and m labels in O(n) steps on max(n\,m) CRCW PR AM processors. Additionally\, it does not perform more work than the sequen tial counterpart.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janmartensaparallelal gorithmforbisimulationpartitionrefinement/ END:VEVENT BEGIN:VEVENT UID:20200922T1259Z1600779549.1628EO7831@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200922T120007Z LASTMODIFIED:20200922T120007Z DTSTART;TZID=Europe/Amsterdam:20200924T124500 DTEND;TZID=Europe/Amsterdam:20200924T133000 SUMMARY: Anna Stramaglia: Deadlock in packet switching networks DESCRIPTION: Deadlock is a historically wellknown bug pattern in computer systems where\, in the most general sense\, a system reaches a state in whi ch it cannot progress any further. In this work\, we investigate deadlocks in packet switching networks with a deterministic routing function. We form alize three different notions of deadlock\, namely\, global\, local and wea k ...continue reading XALTDESC;FMTTYPE=text/html:Deadlock is a historically wellknown bug pattern in computer systems where\, in the most general sense\, a system re aches a state in which it cannot progress any further. In this work\, we in vestigate deadlocks in packet switching networks with a deterministic routi ng function. We formalize three different notions of deadlock\, namely\, gl obal\, local and weak deadlock. We formally define the relation between the se different notions. Moreover\, we formalize packet switching networks in nuXmv and verify them for each of the notions of deadlock\, based on the th eory proposed. We also explore the translation of these networks to xMAS. CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/annastramagliadeadlock inpacketswitchingnetworks/ END:VEVENT BEGIN:VEVENT UID:20200921T0703Z1600671807.3597EO7801@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200921T065519Z LASTMODIFIED:20200921T065638Z DTSTART;TZID=Europe/Amsterdam:20200921T133000 DTEND;TZID=Europe/Amsterdam:20200921T140000 SUMMARY: Nikita Golovliov: Verification of Multiprocessor System Memory Mod el DESCRIPTION: In a shared memory multiprocessor system\, the memory model de termines the outcome of read operations at any time\, given a partial order of memory operations induced by processorissued writes and reads. A memor y model may pertain to highlevel language semantics or hardware program ex ecution. This thesis focuses on verification of hardware memory model confo rmance\, i.e. ...continue reading XALTDESC;FMTTYPE=text/html:
In a shared memory multiprocessor system \, the memory model determines the outcome of read operations at any time\, given a partial order of memory operations induced by processorissued wri tes and reads. A memory model may pertain to highlevel language semantics or hardware program execution.
This thesis focuses on verification of hardware memory model conformance\, i.e. given a hardware specification an d memory model\, verifying whether all the possible executions of any progr am on the hardware are permitted by the memory model\, and vice versa.
< p>Viewbased definitions of a memory model require existence of a certain o rder between memory modification and observation events\, called view. If\, and only if\, there exists a view that is consistent with the memory model for every execution of any program by a multiprocessor system\, then the m ultiprocessor system conforms to the memory model.Given a generic hi ghlevel processormemory interface\, we provide a translation of the relea se consistency hardware memory model to a set of linear temporal logic prop erties. We analyse the correctness of the translation and the deficiencies of the approach. We discuss the relation of the hardware memory model to th e memory model of C++.
We provide an example multiprocessor system de sign that is used for verifica tion of memory model conformance\, and the guidelines for applying the properties to a realworld system.
We present a general method to verify an m CRL2 model of a multiprocessor with respect to memory consistency and prove the correctness of this method.
Consequently\, we present a way to r eformulate most memory models that are defined in terms of serial views usi ng observations. We prove that any execution of a program by a multiprocess or satisfying this formulation is memory consistent under the original memo ry consistency model. We then express this as a set of predicates on the tr aces allowed by an mCRL2 model and prove that if all traces allowed by the mCRL2 model satisfy these predicates\, then all executions allowed by the mCRL2 model are consistent with respect to the original memory consistency model.
We also formulate a subset of the C++ memory model in terms of serial views. We prove that if such that serial view exists for every exec ution allowed by a multiprocessor\, then every execution allowed by that pr ocessor is consistent under the C++ memory model. The predicates on mCRL2 t races are then expressed as mucalculus formulas and are used to verify an mCRL2 model of a multiprocessor with respect to local consistency and cache consistency\, which are subsets of the serial view representing the C++ me mory model. We use these mucalculus formulas to benchmark the verification an example CPU model using the mCRL2 toolset.
CATEGORIES:MSc Defence LOCATION:Atlas 2.215 GEO:52.374540;4.897976 ORGANIZER;CN="Jeroen Keiren":MAILTO:j.j.a.keiren@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/wesselsinnemaverifying memoryconsistencyinmcrl2/ END:VEVENT BEGIN:VEVENT UID:20200921T0641Z1600670472.1065EO7781@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200921T063251Z LASTMODIFIED:20200921T063251Z DTSTART;TZID=Europe/Amsterdam:20200917T124500 DTEND;TZID=Europe/Amsterdam:20200917T133000 SUMMARY: Alexander Fedotov: Effective System Level Liveness Verification DESCRIPTION: The language xMAS has been designed by Intel with the purpose of modelling and verification of hardware. Recently\, the language was exte nded with finite state machines to make it more expressive. Furthermore\, i t was shown how to prove liveness of such extended xMAS networks. Unfortuna tely\, we demonstrate that the proof technique is unsound. We provide ...co ntinue reading XALTDESC;FMTTYPE=text/html:The language xMAS has been designed by Int el with the purpose of modelling and verification of hardware. Recently\, t he language was extended with finite state machines to make it more express ive. Furthermore\, it was shown how to prove liveness of such extended xMAS networks. Unfortunately\, we demonstrate that the proof technique is unsou nd. We provide an alternative approach which we have carefully proven to be correct. Moreover\, we show that our approach scales very well\, which mak es it possible to prove liveness properties at the system level. In particu lar\, we show that using our approach\, it is possible to verify a power co ntrol architecture composed of 1299 state machines representing 50 power do mains where each domain contains 5 master and 5 slave devices. Proving live ness of this system takes less than 10 minutes.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/alexanderfedotoveffecti vesystemlevellivenessverification/ END:VEVENT BEGIN:VEVENT UID:20200826T1606Z1598457975.1003EO6801@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200826T135859Z LASTMODIFIED:20200826T140530Z DTSTART;TZID=Europe/Amsterdam:20200916T160000 DTEND;TZID=Europe/Amsterdam:20200916T173000 SUMMARY: Thomas Neele: Reductions for Parity Games and Model Checking DESCRIPTION: On September 16th 2020\, Thomas Neele will defend his thesis t itle ‘Reductions for Parity Games and Model Checking’\, which is available here. The defence will be streamed online via MS Teams. The link to the str eam is available on request from t.s.neele@tue.nl. XALTDESC;FMTTYPE=text/html:On September 16th 2020\, Thomas Neele will defend his thesis title 'Reductions for Parity Games and Model Checking'\, which is available here. The defence will be str eamed online via MS Teams. The link to the stream is available on request f rom t.s.neele@tue.nl.
CATEGORIES:PhD Defence LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Thomas Neele":MAILTO:t.s.neele@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/phddefensethomasneele/ END:VEVENT BEGIN:VEVENT UID:20200909T1004Z1599645857.195EO7741@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200909T081944Z LASTMODIFIED:20200909T081944Z DTSTART;TZID=Europe/Amsterdam:20200910T124500 DTEND;TZID=Europe/Amsterdam:20200910T133000 SUMMARY: Ferry Timmers: ASD\, the good\, the bad\, and the ugly. DESCRIPTION: The ASD framework\, a proprietary standard for model driven en gineering\, has been around for over a decade now. It provides a toolset to design and verify control systems\, and has successfully been employed by the industry. We look at the formalisms to see what makes it tick\; the adv antages of using ASD\, its limitations\, and ...continue reading XALTDESC;FMTTYPE=text/html:The ASD framework\, a proprietary standard for model driven engineering\, has been around for over a decade now. It p rovides a toolset to design and verify control systems\, and has successful ly been employed by the industry. We look at the formalisms to see what mak es it tick\; the advantages of using ASD\, its limitations\, and problems t hat may rise. The goal is to give a more general impression of ASD\, rather than a detailed explanation.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ferrytimmersasdthegoo dthebadandtheugly/ END:VEVENT BEGIN:VEVENT UID:20200817T1242Z1597668139.8341EO7661@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200817T122247Z LASTMODIFIED:20200817T122709Z DTSTART;TZID=Europe/Amsterdam:20200818T153000 DTEND;TZID=Europe/Amsterdam:20200818T160000 SUMMARY: Sebastiaan Verhoek: SMT solver verification of ladder logic in a p roduction environment (Tata Steel) DESCRIPTION: It is shown how to verify requirements on the PLC code in use at Tata Steel. A translator from PLC programs to the input language for SMT solvers has been written. Subsequently\, requirements on some of the large st PLC programs available at Tata steel have been written down\, and their validity on the software has ...continue reading XALTDESC;FMTTYPE=text/html:It is shown how to verify requirements on the PLC code in use at Tata Steel. A translator from PLC programs to the in put language for SMT solvers has been written. Subsequently\, requirements on some of the largest PLC programs available at Tata steel have been writt en down\, and their validity on the software has been validated.
CATEGORIES:MSc Defence LOCATION:Atlas 2.320 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/sebastiaanverhoeksmtso lververificationofladderlogicinaproductionenvironmenttatasteel/ END:VEVENT BEGIN:VEVENT UID:20200624T0925Z1592990707.2201EO7361@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200624T083345Z LASTMODIFIED:20200624T083345Z DTSTART;TZID=Europe/Amsterdam:20200625T124500 DTEND;TZID=Europe/Amsterdam:20200625T133000 SUMMARY: Anton Wijs: Term Rewriting on GPUs DESCRIPTION: We are interested in finding a programming model to employ the power of Graphics Processing Units (GPUs) more easily than via traditional programming. We propose to express computations in the form of term rewrit e systems. We present a way to implement term rewriting on a GPU. We do thi s by letting the GPU repeatedly perform ...continue reading XALTDESC;FMTTYPE=text/html:This presentation is the third in the cont ext of our work on OIL\, a language for modelling control software\, where we have enabled the use of model checking via a translation to mCRL2. In th is presentation we will dive a bit deeper into the complexity of this trans lation. Also\, to test the feasibility of our methods we have applied them to a second model from Canon\, which is considerably larger than the one di scussed in the previous presentation. We will discuss what issues we have e ncountered while doing so and how we solved them.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/olavbunteformalverific ationofoilcomponentspecificationsusingmcrl2/ END:VEVENT BEGIN:VEVENT UID:20200610T1416Z1591798619.0243EO7231@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200610T134746Z LASTMODIFIED:20200610T134746Z DTSTART;TZID=Europe/Amsterdam:20200611T124500 DTEND;TZID=Europe/Amsterdam:20200611T133000 SUMMARY: Jeroen Keiren: Extensible Proof Systems for InfiniteState Systems DESCRIPTION: In the early 90’s\, Bradfield & Stirling developed a sound and complete tableau method for proving that sets of states in infinitestate labelled transition systems satisfy formulas in the modal mucalculus. Unfo rtunately\, the soundness proof they presented is not extensible in the fol lowing sense. First\, it is hard to add new modalities to the mucalculus\, ...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. Since manual rejuvenation of such sys tems is costly and cumbersome\, metaprogramming techniques can be used to decrease this effort. Generic transformations\, however\, do not take domai n knowledge into account and are therefore not satisfactory. In this talk\, I will discuss an ongoing project I'm conducting together with Philips Hea lthcare\, in which we perform a significant refactoring on a part of their codebase. I will highlight how we have broken up this refactoring in smalle r transformations\, and how we evaluate the quality of each intermediate st ep.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rodinaarssenassessingt hequalityofadhocrefactorings/ END:VEVENT BEGIN:VEVENT UID:20200506T2217Z1588803469.7411EO7121@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200506T220155Z LASTMODIFIED:20200506T220155Z DTSTART;TZID=Europe/Amsterdam:20200507T124500 DTEND;TZID=Europe/Amsterdam:20200507T133000 SUMMARY: Rick Erkens: Optimising adaptive nonlinear pattern matching autom ata DESCRIPTION: This presentation builds on a previous presentation by Maurice Laveaux that was titled ‘adaptive nonlinear pattern matching automata’. P attern matching is a fundamental problem in many areas of computing science \, both practical and theoretical. Given a large finite set of firstorder patterns and a term t\, we are interested in an efficient way to find all . ..continue reading XALTDESC;FMTTYPE=text/html:This presentation builds on a previous pre sentation by Maurice Laveaux that was titled 'adaptive nonlinear pattern m atching automata'.
Pattern matching is a fundamental problem in many areas of computing science\, both practical and theoretical. Given a large finite set of firstorder patterns and a term t\, we are interested in an e fficient way to find all pattern matches for t. In the previous presentatio n we proposed adaptive nonlinear pattern matching automata (ANPMA) as an e xtension of earlier work on adaptive pattern matching automata by Sekar et al. By preprocessing the given pattern set and constructing an automaton\, it is possible to solve the matching problem by only inspecting every posit ion of term t at most once. In a setting where the pattern set is fixed and the matching problem has to be decided many times\, it is crucial for perf ormance to have such an automaton. The method that we proposed is not optim al yet. The construction algorithm can yield states that are redundant. The se redundancies are due to the fact that function symbol checks can give in formation about consistency checks and vice versa. The relation between the se two kinds of checks is not clear yet. In this presentation I will talk a bout a solution that we have in mind to compute an optimal ANPMA on the fly . The work on ANPMA will be presented at FSCD 2020. The extension that I wi ll talk about next thursday is still a work in progress.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/rickerkensoptimisingad aptivenonlinearpatternmatchingautomata/ END:VEVENT BEGIN:VEVENT UID:20200428T1140Z1588074054.1776EO7101@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200428T113326Z LASTMODIFIED:20200428T113326Z DTSTART;TZID=Europe/Amsterdam:20200430T124500 DTEND;TZID=Europe/Amsterdam:20200430T133000 SUMMARY: Hans Zantema: Computation of complexity of automatic sequences DESCRIPTION: In an earlier talk the complexity of an automatic sequence was presented as the minimal size of an automaton describing the sequence. Mor e precisely\, the nth element of the binary sequence is 1 if and only if t he binary representation of n is accepted by the automaton. On this notion some main properties were investigated. In ...continue reading XALTDESC;FMTTYPE=text/html:In an earlier talk the complexity of an au tomatic sequence was presented as the minimal size of an automaton describi ng the sequence. More precisely\, the nth element of the binary sequence i s 1 if and only if the binary representation of n is accepted by the automa ton. On this notion some main properties were investigated. In the meantime a paper on this work has been accepted for the LATA 2020 conference\, and was honored by the best paper award. After a recap of the main notions and properties\, in this talk the focus will be on how to compute the correspon ding minimal automaton automatically from a prefix of the sequence\, by mea ns of SMT solving\, and on criteria on how long this prefix should be.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/hanszantemacomputation ofcomplexityofautomaticsequences/ END:VEVENT BEGIN:VEVENT UID:20200422T0825Z1587543917.3972EO7091@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200421T201805Z LASTMODIFIED:20200421T201805Z DTSTART;TZID=Europe/Amsterdam:20200423T124500 DTEND;TZID=Europe/Amsterdam:20200423T133000 SUMMARY: Maurice Laveaux: Decompositional Minimization of Monolithic Proces ses DESCRIPTION: Title: Decompositional Minimization of Monolithic Processes Ab stract: Compositional minimization is another established technique to tack le the state space explosion problem. This technique attempts to use the pa rallel processes defined in the highlevel specification to obtain a reduce d state space w.r.t some behavioural equivalence immediately without explor ing the whole state space first. This technique would also ...continue read ing XALTDESC;FMTTYPE=text/html:Title: Decompositional Minimization of Mon olithic Processes
Abstract: Compositional minimization is another est ablished technique to tackle the state space explosion problem. This techni que attempts to use the parallel processes defined in the highlevel specif ication to obtain a reduced state space w.r.t some behavioural equivalence immediately without exploring the whole state space first. This technique w ould also be a useful addition for the mCRL2 toolset. However\, applying th is technique within the context of mCRL2 is hindered by the fact that we ty pically first transform the given specification into a monolithic process w here all parallel composition has been removed. Avoiding this transformatio n is undesirable\, because it facilitates various other static analysis tec hniques that might reduce the state space. Therefore\, we propose a method to decompose the resulting monolithic process\, where other simplification techniques could be applied first\, into a number of parallel processes suc h that the compositional minimization technique is applicable again.
CATEGORIES:Colloquium LOCATION:MS Teams GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/mauricelaveauxdecomposi tionalminimizationofmonolithicprocesses/ END:VEVENT BEGIN:VEVENT UID:20200414T1406Z1586873185.6511EO7081@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200414T132541Z LASTMODIFIED:20200414T132541Z DTSTART;TZID=Europe/Amsterdam:20200416T124500 DTEND;TZID=Europe/Amsterdam:20200416T133000 SUMMARY: Thomas Neele: PartialOrder Reduction for Parity Games with an App lication on Parameterised Boolean Equation Systems DESCRIPTION: Partialorder reduction (POR) is a wellestablished technique to combat the problem of statespace explosion. We propose POR techniques t hat are sound for parity games\, a wellestablished formalism for solving a variety of decision problems. As a consequence\, we obtain the first POR m ethod that is sound for model checking for the full modal mucalculus. Our ...continue reading XALTDESC;FMTTYPE=text/html:Partialorder reduction (POR) is a welles tablished technique to combat the problem of statespace explosion. We prop ose POR techniques that are sound for parity games\, a wellestablished for malism for solving a variety of decision problems. As a consequence\, we ob tain the first POR method that is sound for model checking for the full mod al mucalculus. Our technique is applied to\, and implemented for the fixed point logic called parameterised Boolean equation systems\, which provides a highlevel representation of parity games. Experiments indicate that sub stantial reductions can be achieved.
CATEGORIES:Colloquium LOCATION:Zoom GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/thomasneelepartialorde rreductionforparitygameswithanapplicationonparameterisedbooleane quationsystems/ END:VEVENT BEGIN:VEVENT UID:20200414T1406Z1586873185.6578EO7071@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200414T132104Z LASTMODIFIED:20200414T132104Z DTSTART;TZID=Europe/Amsterdam:20200409T124500 DTEND;TZID=Europe/Amsterdam:20200409T133000 SUMMARY: Freek Verbeek: Formal Proofs of Return Address Integrity DESCRIPTION: We present a methodology for generating a characterization of the memory used by an assembly program\, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of mem ory usage is required for compositional reasoning over assembly programs. M oreover\, it can be used to prove lowlevel security ...continue reading XALTDESC;FMTTYPE=text/html:We present a methodology for generating a characterization of the memory used by an assembly program\, as well as a f ormal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover\, it can be used to prove lowlevel security pr operties\, such as integrity of the return address of a function. Our verif ication method is based on interactive theorem proving\, but provides autom ation by generating pre and postconditions\, invariants\, controlflow\, a nd assumptions on memory layout. As a case study\, three binaries of the Xe n hypervisor are disassembled. These binaries are the result of a complex b uildchain compiling production code\, and contain various complex and nest ed loops\, large and compound data structures\, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functio ns\, covering 12\,252 assembly instructions.
CATEGORIES:Colloquium LOCATION:Zoom GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/freekverbeekformalproo fsofreturnaddressintegrity/ END:VEVENT BEGIN:VEVENT UID:20200414T1406Z1586873185.6607EO7061@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200414T131644Z LASTMODIFIED:20200414T131733Z DTSTART;TZID=Europe/Amsterdam:20200402T124500 DTEND;TZID=Europe/Amsterdam:20200402T133000 SUMMARY: Bas Luttik: Supporting railway infrastructure managers with formal models and analyses DESCRIPTION: In this talk\, I will discuss our recent experiences with usin g the mCRL2 toolset – which has a processalgebra based modelling language\ , a modal mucalculusbased property language\, and an explicitstate model checker – to support two major innovation activities from railway infrastr ucture managers. First\, there is the EULYNX initiative of the European rai lway infrastructure managers. ...continue reading XALTDESC;FMTTYPE=text/html:In this talk\, I will discuss our recent e xperiences with using the mCRL2 toolset  which has a processalgebra based modelling language\, a modal mucalculusbased property language\, and an explicitstate model checker  to support two major innovation activities f rom railway infrastructure managers.
First\, there is the EULYNX init iative of the European railway infrastructure managers. The aim of EULYNX i s to standardise the interfaces between the interlocking and field elements (signals\, points\, level crossings)\; these interface standards are model led in SysML. In a project funded by the Dutch and German railway infrastru cture managers we are translating the SysML models to mCRL2 not only to for mally assess the quality of the standard by model checking\, but also to fa cilitate using them for modelbased testing of compliance to the standard o f delivered components.
Second\, in collaboration with the Dutch rail way infrastructure manager ProRail we have formally modelled and analysed t he ERTMS Hybrid Level 3 principles. These principles facilitate subdividing track sections into virtual subsections\, in order to allow multiple train s simultaneously on the same track section\, thus increasing capacity. We h ave plans to support ProRail developers in their further elaboration of the design and implementation of ERTMS Hybrid Level 3.
CATEGORIES:Colloquium LOCATION:Zoom GEO:52.374540;4.897976 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/basluttiksupportingrai lwayinfrastructuremanagerswithformalmodelsandanalyses/ END:VEVENT BEGIN:VEVENT UID:20200303T1238Z1583239107.7407EO6921@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200303T123149Z LASTMODIFIED:20200303T123149Z DTSTART;TZID=Europe/Amsterdam:20200305T124500 DTEND;TZID=Europe/Amsterdam:20200305T133000 SUMMARY: Jan Martens: Resynchronizability of origin transducers DESCRIPTION: Origin semantics introduced by Bojańczyk is a fine grained sem antics for transducers\, that not only expresses the relation between input and output words\, but also includes a function that given an output posit ion returns the input position where it was produced: the origin. In this t alk we’ll discuss resynchronizations\, a tool to relax the notion ...contin ue reading XALTDESC;FMTTYPE=text/html:
Origin semantics introduced by Bojańczyk i s a fine grained semantics for transducers\, that not only expresses the re lation between input and output words\, but also includes a function that g iven an output position returns the input position where it was produced: t he origin. In this talk we'll discuss resynchronizations\, a tool to relax the notion of origin while maintaining decidable properties. The talk speci fically focusses on the notion of containment upto some unknown resynchron ization. This relation forms a preorder strictly in between classical and origin containment. We show this containment is undecidable\, which was a r ecent open problem. This is done using a notion of limited traversal which syntactically classifies the nonexistence of a resynchronization.
CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/janmartensresynchroniza bilityoforigintransducers/ END:VEVENT BEGIN:VEVENT UID:20200218T2105Z1582059933.0252EO6871@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200218T152034Z LASTMODIFIED:20200218T152034Z DTSTART;TZID=Europe/Amsterdam:20200220T124500 DTEND;TZID=Europe/Amsterdam:20200220T133000 SUMMARY: Ferry Timmers: Maintaining strongly connected components efficient ly\, under edge deletions DESCRIPTION: Assume we have a directed graph. We can find the strongly conn ected components in this graph using for instance Tarjan’s algorithm. Let’s say we remove an edge from the graph. Can we recalculate the SCCs? A (rece nt) paper by Bernstein\, Probst et.al. presents a way tot do this efficient ly. I’ll roughly discuss my experiences with ...continue reading XALTDESC;FMTTYPE=text/html:Assume we have a directed graph. We can fi nd the strongly connected components in this graph using for instance Tarja n's algorithm. Let's say we remove an edge from the graph. Can we recalcula te the SCCs? A (recent) paper by Bernstein\, Probst et.al. presents a way t ot do this efficiently. I'll roughly discuss my experiences with the algori thm and then focus on EStrees\, a clever data structure the algorithm exte nded.
CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/ferrytimmersmaintaining stronglyconnectedcomponentsefficientlyunderedgedeletions/ END:VEVENT BEGIN:VEVENT UID:20200219T1954Z1582142088.944EO6891@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200219T190328Z LASTMODIFIED:20200219T190328Z DTSTART;TZID=Europe/Amsterdam:20200219T143000 DTEND;TZID=Europe/Amsterdam:20200219T151500 SUMMARY: Elbert van de Put: Ant Colony Optimization for Model Checking DESCRIPTION: Ant Colony Optimization is an optimization algorithm that is i nspired by the foraging behavior of ants. In this thesis I have applied Ant Colony Optimization to problems that are generated from the model checking problem\, to Boolean equation systems and to parity games. The results of this research are mixed but we have discovered approaches ...continue readi ng XALTDESC;FMTTYPE=text/html:Ant Colony Optimization is an optimization algorithm that is inspired by the foraging behavior of ants. In this thesi s I have applied Ant Colony Optimization to problems that are generated fro m the model checking problem\, to Boolean equation systems and to parity ga mes. The results of this research are mixed but we have discovered approach es where further research seems promising.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 2 GEO:51.447551;5.487453 ORGANIZER;CN="Erik de Vink":MAILTO:e.p.d.vink@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/elbertvandeputantcol onyoptimizationformodelchecking/ END:VEVENT BEGIN:VEVENT UID:20200211T1329Z1581427763.0372EO6861@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200211T122925Z LASTMODIFIED:20200211T122925Z DTSTART;TZID=Europe/Amsterdam:20200213T124500 DTEND;TZID=Europe/Amsterdam:20200213T133000 SUMMARY: Mark Bouwman: Verification and modelbased testing of a railway po int/switch using mCRL2 DESCRIPTION: The EULYNX initiative is a collaborative effort of more than t en European railway infrastructure managers to standardise signalling inter faces. Within EULYNX\, FormaSig aims to use formal methods to analyse the c orrectness of the standard. We have recently concluded a case study in whic h we translate the EULYNX Point interface from SysML to mCRL2. The resultin g ...continue reading XALTDESC;FMTTYPE=text/html:The EULYNX initiative is a collaborative e ffort of more than ten European railway infrastructure managers to standard ise signalling interfaces. Within EULYNX\, FormaSig aims to use formal meth ods to analyse the correctness of the standard. We have recently concluded a case study in which we translate the EULYNX Point interface from SysML to mCRL2. The resulting mCRL2 model is subsequently used to contribute to the quality of the standard by verifying whether important safety requirements hold for the model. Test cases have been automatically derived from the sa me mCRL2 model. They have been executed\, effectively checking whether an a ctual Point implementation conforms to the EULYNX standard. This talk will discuss the case study itself and the lessons learned concerning formalisin g SysML and applying formal methods in the railway domain.
CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/markbouwmanverification andmodelbasedtestingofarailwaypointswitchusingmcrl2/ END:VEVENT BEGIN:VEVENT UID:20200204T1113Z1580814815.9488EO6841@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200204T103823Z LASTMODIFIED:20200204T103823Z DTSTART;TZID=Europe/Amsterdam:20200206T124500 DTEND;TZID=Europe/Amsterdam:20200206T133000 SUMMARY: Jan Bergstra: From computability theory to computer science and ba ck DESCRIPTION: I will discuss the sequence of themes which I have been resear ching since 1973\, and try to highlight how research questions have come\, and gone and reappeared. I will provide concise phrasings of leading princi ples which I have made use of in successive stages\, and how and why these have changed. Finally I will discuss ...continue reading XALTDESC;FMTTYPE=text/html:I will discuss the sequence of themes whic h I have been researching since 1973\, and try to highlight how research qu estions have come\, and gone and reappeared. I will provide concise phrasin gs of leading principles which I have made use of in successive stages\, an d how and why these have changed. Finally I will discuss how the context of research changes (for the better) upon my "emeritaat"\, now 3 years ago. 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/janbergstrafromcomputa bilitytheorytocomputerscienceandback/ END:VEVENT BEGIN:VEVENT UID:20200121T1541Z1579621268.5902EO6781@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200121T141151Z LASTMODIFIED:20200121T141151Z DTSTART;TZID=Europe/Amsterdam:20200123T124500 DTEND;TZID=Europe/Amsterdam:20200123T133000 SUMMARY: Jeroen Keiren: The basics of hardware verification using xMAS DESCRIPTION: xMAS is a graphical specification language that allows to desc ribe hardware components such as communication fabrics by composing microar chitectural primitives such as queues. Hardware components described using xMAS are sufficiently precise to allow formal verification\, however\, the explicit state space of such components suffers from the state space explos ion problem. Therefore\, other verification techniques have ...continue rea ding XALTDESC;FMTTYPE=text/html:
xMAS is a graphical specification language that allows to describe hardware components such as communication fabrics by composing microarchitectural primitives such as queues. Hardware compone nts described using xMAS are sufficiently precise to allow formal verificat ion\, however\, the explicit state space of such components suffers from th e state space explosion problem. Therefore\, other verification techniques have been described in the literature. In particular\, sound (but not compl ete) approaches have been devised that translate the lack of liveness (some times referred to as the presence of a local deadlock) to SAT or SMT. In th is talk I will discuss the main aspects of the semantics of xMAS networks\, and I will discuss my understanding of some of the existing verification a pproaches.
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/jeroenkeirenthebasics ofhardwareverificationusingxmas/ END:VEVENT BEGIN:VEVENT UID:20200115T1203Z1579089786.7184EO6771@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200115T105130Z LASTMODIFIED:20200115T105233Z DTSTART;TZID=Europe/Amsterdam:20200116T124500 DTEND;TZID=Europe/Amsterdam:20200116T133000 SUMMARY: Rodin Aarssen: HighFidelity Metaprogramming with Separator Syntax Trees DESCRIPTION: Many metaprogramming tasks\, such as refactorings\, automated bug fixing\, or largescale software renovation\, require highfidelity sou rce code transformations – transformations which preserve comments and layo ut as much as possible. Abstract syntax trees (ASTs) typically abstract fro m such details\, and hence would require pretty printing\, destroying the o riginal program layout. Concrete syntax trees (CSTs) preserve all layout in formation\, ...continue reading XALTDESC;FMTTYPE=text/html:Many metaprogramming tasks\, such as refac torings\, automated bug fixing\, or largescale software renovation\, requi re highfidelity source code transformations – transformations which preser ve comments and layout as much as possible. Abstract syntax trees (ASTs) ty pically abstract from such details\, and hence would require pretty printin g\, destroying the original program layout. Concrete syntax trees (CSTs) pr eserve all layout information\, but transformation systems or parsers that support CSTs are rare and can be cumbersome to use. In this talk I will pre sent separator syntax trees (SSTs)\, a lightweight syntax tree format\, tha t sits between AST and CSTs\, in terms of the amount of information they pr eserve. SSTs extend ASTs by recording textual layout information separating AST nodes. This information can be used to reconstruct the textual code af ter parsing\, but can largely be ignored when implementing highfidelity tr ansformations.
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/rodinaarssenhighfideli tymetaprogrammingwithseparatorsyntaxtrees/ END:VEVENT BEGIN:VEVENT UID:20200107T1320Z1578403252.1452EO6751@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20200107T130837Z LASTMODIFIED:20200107T130837Z DTSTART;TZID=Europe/Amsterdam:20200109T124500 DTEND;TZID=Europe/Amsterdam:20200109T133000 SUMMARY: Wieger Wesselink: A Dafny proof of Tarjan’s strongly connected com ponents algorithm DESCRIPTION: The mCRL2 toolset uses Tarjan’s strongly connected components algorithm at several places. To gain experience with automated provers\, we have made a proof of this algorithm using Dafny\, an automatic program ver ifier. In this talk I will explain our solution\, and tell something about our experiences with Dafny. This is joint work with Kees Huizing. XALTDESC;FMTTYPE=text/html:The mCRL2 toolset uses Tarjan's strongly c onnected components algorithm at several places. To gain experience with au tomated provers\, we have made a proof of this algorithm using Dafny\, an a utomatic program verifier. In this talk I will explain our solution\, and t ell something about our experiences with Dafny.
This is joint work wi th Kees Huizing.
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/wiegerwesselinkadafny proofoftarjansstronglyconnectedcomponentsalgorithm/ END:VEVENT BEGIN:VEVENT UID:20191217T0925Z1576574716.7118EO6541@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191217T091544Z LASTMODIFIED:20191217T091544Z DTSTART;TZID=Europe/Amsterdam:20191219T124500 DTEND;TZID=Europe/Amsterdam:20191219T133000 SUMMARY: Rick Erkens: Abstraction for Bisimulation up to Context DESCRIPTION: Abstract: Roughly one year ago I gave a colloquium talk about upto techniques for branching bisimilarity. In particular we discussed the soundness of branching bisimilarity up to context for CCS with guarded sum s. In combination with other upto techniques this result allows for more f easible proofs when attempting to prove two CCS terms bisimilar. We added . ..continue reading XALTDESC;FMTTYPE=text/html:Abstract:
Roughly one year ago I gav e a colloquium talk about upto techniques for branching bisimilarity. In p articular we discussed the soundness of branching bisimilarity up to contex t for CCS with guarded sums. In combination with other upto techniques thi s result allows for more feasible proofs when attempting to prove two CCS t erms bisimilar. We added two levels of abstraction to this result\, yieldin g the same result for a larger class of process algebras and allowing for e asier instantiation to other notions of bisimilarity that abstract from sil ent transitions. The first level involves Bloom's cool congruence formats. The second level involves a bialgebraic approach\, which will be the main f ocus of this talk.
Based on joint work with Jurriaan Rot and Bas Lutt ik.
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/rickerkensabstractionf orbisimulationuptocontext/ END:VEVENT BEGIN:VEVENT UID:20191211T0921Z1576056095.4876EO6531@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191211T091734Z LASTMODIFIED:20191211T091734Z DTSTART;TZID=Europe/Amsterdam:20191212T124500 DTEND;TZID=Europe/Amsterdam:20191212T133000 SUMMARY: Tim Willemse: FamilyBased SPL Model Checking Using Parity Games w ith Variability DESCRIPTION: We propose efficient familybased Software Product Lines (SPL) model checking based on variability parity games. These extend parity gam es with conditional edges labelled with (feature) configurations. We valida te our contribution by experiments on SPL benchmark models\, which demonstr ate that a novel familybased algorithm to collectively solve variability p arity games\, using symbolic representations of the configuration ...contin ue reading XALTDESC;FMTTYPE=text/html:OIL is a domainspecific language under de velopment at Océ for specifying\, analysing\, and implementing software com ponents. OIL is to have IDE support\, transformations to formal modelling l anguages for requirement verification\, and code generation towards general purpose languages such as C++. Modelbased testing is an approach to test whether the behaviour of an implementation conforms to the behaviour descri bed in a formal model. A notable benefit of this approach is the automated test derivation and execution. This master thesis presents a C++ code gener ator for OIL\, implemented in the Spoofax language workbench. The correctne ss of the code generator is validated by means of modelbased testing\, imp lemented in JTorX.
CATEGORIES:MSc Defence 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/markfrenkencodegenerat ionandmodelbasedtestingincontextofoil/ END:VEVENT BEGIN:VEVENT UID:20191204T1338Z1575466733.2534EO6491@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191204T124753Z LASTMODIFIED:20191204T124753Z DTSTART;TZID=Europe/Amsterdam:20191205T124500 DTEND;TZID=Europe/Amsterdam:20191205T133000 SUMMARY: Olav Bunte: Validity of OIL component specifications DESCRIPTION: With OIL one can model the desired behaviour of a system with a protocol specification and the actual behaviour of a component with a com ponent specification. To choose what events to execute\, an OIL component u ses a scheduler with runtocompletion semantics. However\, to avoid undesi red behaviour concerning this scheduler\, we need to put some validity ...c ontinue reading XALTDESC;FMTTYPE=text/html:With OIL one can model the desired behavio ur of a system with a protocol specification and the actual behaviour of a component with a component specification. To choose what events to execute\ , an OIL component uses a scheduler with runtocompletion semantics. Howev er\, to avoid undesired behaviour concerning this scheduler\, we need to pu t some validity requirements on an OIL component specification. In this pre sentation we show what requirements these are and how they can be checked o n an OIL component specification.
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/olavbuntevalidityofoi lcomponentspecifications/ END:VEVENT BEGIN:VEVENT UID:20191126T1058Z1574765935.9939EO6411@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191126T104250Z LASTMODIFIED:20191126T104250Z DTSTART;TZID=Europe/Amsterdam:20191128T124500 DTEND;TZID=Europe/Amsterdam:20191128T133000 SUMMARY: Maurice Laveaux: Adaptive Nonlinear Pattern Match Automata DESCRIPTION: Efficient pattern matching is fundamental for practical term r ewrite engines. By preprocessing the given patterns into a finite determini stic automaton the matching patterns can be decided in a single traversal o f the relevant parts of the input term. Most of the existing automaton base d techniques are restricted to linear patterns\, where each variable occurs at ...continue reading XALTDESC;FMTTYPE=text/html:Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns int o a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of the input term. Most of the exi sting automaton based techniques are restricted to linear patterns\, where each variable occurs at most once\, and require an additional postprocessi ng step to check variable consistency. However\, interleaving the variable consistency and pattern matching phases can reduce the number of steps requ ired to find a match. Therefore\, we introduce consistency automata to dete rmine variable consistency using an optimal number of comparisons. These co nsistency automata are then combined with existing socalled adaptive patte rn match automata as introduced by Sekar et al. We show that the resulting automata can solve the pattern matching problem correctly\, and more effici ently then existing approaches.
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/mauricelaveauxadaptive nonlinearpatternmatchautomata/ END:VEVENT BEGIN:VEVENT UID:20191118T1425Z1574087113.204EO6231@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191118T142420Z LASTMODIFIED:20191118T142420Z DTSTART;TZID=Europe/Amsterdam:20191121T124500 DTEND;TZID=Europe/Amsterdam:20191121T133000 SUMMARY: Thomas Neele: The Inconsistent Labelling Problem of StutterPreser ving PartialOrder Reduction DESCRIPTION: In model checking\, partialorder reduction (POR) is an effect ive technique to reduce the size of the state space. Stubborn sets are an e stablished variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is ...continue reading XALTDESC;FMTTYPE=text/html:In model checking\, partialorder reductio n (POR) is an effective technique to reduce the size of the state space. St ubborn sets are an established variant of POR and have seen many applicatio ns over the past 31 years. One of the early works on stubborn sets shows th at a combination of several conditions on the reduction is sufficient to pr eserve stuttertrace equivalence\, making stubborn sets suitable for model checking of lineartime properties. In this paper\, we identify a flaw in t he reasoning and show with a counterexample that stuttertrace equivalence is not necessarily preserved. We propose a solution and analyse in which f ormalisms this problem may occur. The impact on practical implementations i s limited\, since they all compute a correct approximation of the theory. CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/thomasneeletheinconsis tentlabellingproblemofstutterpreservingpartialorderreduction/ END:VEVENT BEGIN:VEVENT UID:20191104T1616Z1572884195.6778EO6211@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191104T160518Z LASTMODIFIED:20191104T160518Z DTSTART;TZID=Europe/Amsterdam:20191107T124500 DTEND;TZID=Europe/Amsterdam:20191107T133000 SUMMARY: Tom Verhoeff: From FP to OO DESCRIPTION: This work got started while teaching a functional programming course\, where I tried to make the abstract concept of F(co)algebras more concrete by stating that\, in Java terms\, these are just classes that imp lement a specific kind of generic interface. To make this even more concret e\, I tried to implement this idea\, together with the ...continue reading XALTDESC;FMTTYPE=text/html:
This work got started while teaching a fun ctional programming course\, where I tried to make the abstract concept of F(co)algebras more concrete by stating that\, in Java terms\, these are j ust classes that implement a specific kind of generic interface. To make th is even more concrete\, I tried to implement this idea\, together with the corresponding (co)inductive type\, that is\, (terminal/)initial F(co)alg ebra. Somewhat to my surprise this worked out quite nicely. I present a sys tematic way of translating inductive types with their catamorphisms (folds) from those types\, and coinductive types with their anamorphisms (unfolds ) into those types\, expressed as functional programs (say in Haskell)\, in to elegant objectoriented code (say in Java). Even types that are inductiv e and coinductive can be handled\, allowing for hylomorphisms (fold after unfold) that are lazy. It turns out that there is a nice way of matching di sjoint sums (coproducts)\, argument patterns\, and F(co)algebras on the FP side with inheritance\, polymorphism+overriding+dynamic dispatch\, and g eneric interfaces on the OO side. What also struck me is that this translat ion provides a legitimate use case for inheritance\, which is often abused (where composition would be more appropriate). I will illustrate this appro ach through some examples (trees\, streams\, and lists)\, while introducing the relevant FP and OO concepts. This serves as a Rosetta stone involving the three formalisms of Haskell\, Category Theory\, and Java. Even if you k now only one of these\, you should be able to grasp the others. The OO impl ementation allows for some useful tradeoffs: memory versus time\, safety a nd easy reasoning versus efficiency and hard reasoning (think: immutable ve rsus mutable). I am working on a FP library for Java based on these ideas. Finally (when time permits)\, I will reflect on this translation and compar e (qualities of) the input FP code with (those of) the resulting OO code\, and with (those of) traditional OO code for the same functionality. I touch upon such qualities as performance\, code size\, maintainability\, and fle xibility.
CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/tomverhoefffromfptoo o/ END:VEVENT BEGIN:VEVENT UID:20191031T0829Z1572510543.9305EO6191@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191031T081055Z LASTMODIFIED:20191031T081055Z DTSTART;TZID=Europe/Amsterdam:20191106T130000 DTEND;TZID=Europe/Amsterdam:20191106T134500 SUMMARY: Sjef van Loo: Verifying SPLs using parity games expressing variabi lity DESCRIPTION: SPL verification can be costly when all the software products of an SPL are verified independently. It is well known that parity games ca n be used to verify software products. We propose a generalization of parit y games\, named variability parity games (VPGs)\, that encode multiple pari ty games in a single game graph decorated with edge ...continue reading XALTDESC;FMTTYPE=text/html:SPL verification can be costly when all th e software products of an SPL are verified independently. It is well known that parity games can be used to verify software products. We propose a gen eralization of parity games\, named variability parity games (VPGs)\, that encode multiple parity games in a single game graph decorated with edge lab els expressing variability between the parity games. We show that a VPG can be constructed from a modal μcalculus formula and an FTS that models the behaviour of the different software products of an SPL. Solving the resulti ng VPG decides for which products in the SPL the formula is satisfied. We i ntroduce several algorithms to efficiently solve VPGs and exploit commonali ties between the different parity games encoded. We perform experiments on SPL models to demonstrate that the VPG algorithms indeed outperform indepen dently verifying every product in an SPL.
CATEGORIES:MSc Defence 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/sjefvanlooverifyingsp lsusingparitygamesexpressingvariability/ END:VEVENT BEGIN:VEVENT UID:20191023T1512Z1571843552.4571EO6151@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191023T143150Z LASTMODIFIED:20191023T143150Z DTSTART;TZID=Europe/Amsterdam:20191024T124500 DTEND;TZID=Europe/Amsterdam:20191024T133000 SUMMARY: Jan Friso Groote: Internally optimized decision diagrams DESCRIPTION: When trying to understand ZDDs\, an alternative to BDDs\, I wa s wondering whether a quite different view on representing boolean function s would be interesting. I called this different view Internally Optimized D ecision Diagrams (IDDs). As it stands it is in no way clear whether this al ternative view would be beneficial to represent large boolean functions\, e specially because I ...continue reading XALTDESC;FMTTYPE=text/html:When trying to understand ZDDs\, an altern ative to BDDs\, I was wondering whether a quite different view on represent ing boolean functions would be interesting. I called this different view In ternally Optimized Decision Diagrams (IDDs). As it stands it is in no way c lear whether this alternative view would be beneficial to represent large b oolean functions\, especially because I have difficulties finding efficient algorithms for standard functions\, such as "and" and "or"\, but I will st ill explain the basic ideas.
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/janfrisogrooteinternal lyoptimizeddecisiondiagrams/ END:VEVENT BEGIN:VEVENT UID:20191007T1513Z1570461220.9654EO6081@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20191007T125627Z LASTMODIFIED:20191007T125627Z DTSTART;TZID=Europe/Amsterdam:20191010T124500 DTEND;TZID=Europe/Amsterdam:20191010T133000 SUMMARY: Vincenzo Ciancia: Spatial Model Checking and Applications to Medic al Image Analysis DESCRIPTION: Spatial aspects of computation are prominent in Computer Scien ce\, especially when dealing with systems distributed in physical space or with image data acquired from various sources. However\, formal verificatio n techniques are usually concerned with temporal properties and do not expl icitly handle spatial information. Our work stems from the topological inte rpretation of modal logics\, the socalled ...continue reading XALTDESC;FMTTYPE=text/html:Spatial aspects of computation are promine
nt in Computer Science\, especially
when dealing with systems distribu
ted in physical space or with image data
acquired from various sources
. However\, formal verification techniques are
usually concerned with
temporal properties and do not explicitly handle spatial
information.<
/p>
Our work stems from the topological interpretation of modal logics\,
the
socalled Spatial Logics. We present a topologybased approach to
model checking
for spatial and spatiotemporal properties. Our results
include theoretical
developments in the more general setting of Cech
closure spaces\, a study of a
"collective" variant\, that has been com
pared to region calculi in recent work\,
publicly available software t
ools\, and some case studies in the setting of smart
transportation.
In recent joint work with the University Hospital of Siena\, we have e
xplored the
application domain of automatic contouring in Medical Imag
ing\, introducing the
tool VoxLogicA\, which merges the stateofthea
rt imaging library ITK with the
unique combination of declarative spec
ification and optimised execution provided
by spatial model checking.
The analysis of an existing benchmark of medical
images for segmentati
on of brain tumours shows that simple VoxLogicA
specifications can rea
ch stateoftheart accuracy\, competing with bestinclass
algorithms
based on machine learning\, with the advantage of explainability and
easy replicability.
References:
Vincenzo Ciancia\, Diego Latell
a\, Michele Loreti\, Mieke Massink:
Model Checking Spatial Logics for
Closure Spaces. Logical Methods in Computer Science 12(4) (2016)
https
://lmcs.episciences.org/2067
Gina Belmonte\, Vincenzo Ciancia\, Diego
Latella\, Mieke Massink:
VoxLogicA: A Spatial Model Checker for Decla
rative Image Analysis. TACAS (1) 2019: 281298
https://link.springer.c
om/chapter/10.1007/9783030174620_16
First order inductive theorem proving deal s with proving new equations based on a given set of equations. More specif ically\, we are interested in proving that the axioms logically imply the g oals. In this presentation I will discuss how we can automate these proofs by induction. The equations can either describe finite or infinite terms. I n this talk we are mainly interested in applying these ideas of induction o n infinite objects. The focus is on the most simple form of infinite object s: infinite sequences of some basic data type. Using a special operator tak e we can also apply our induction techniques on infinite data. Finally we d escribe how our techniques can be implemented in practice.
CATEGORIES:MSc Defence LOCATION:MetaForum MF 7.084 GEO:51.447532;5.487437 ORGANIZER;CN="Hans Zantema":MAILTO:h.zantema@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/stanroelofsautomaticall yprovingequalityofinfinitesequences/ END:VEVENT BEGIN:VEVENT UID:20190925T1434Z1569422058.5098EO6031@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190925T140236Z LASTMODIFIED:20190925T140236Z DTSTART;TZID=Europe/Amsterdam:20190926T124500 DTEND;TZID=Europe/Amsterdam:20190926T133000 SUMMARY: Anton Wijs: Modular Indirect Pushbutton Formal Verification of Mu ltithreaded Code Generators DESCRIPTION: In modeldriven development\, the automated generation of a mu ltithreaded program based on a model specifying the intended system behavi our is an important step. Verifying that such a generation step semanticall y preserves the specified functionality is hard. In related work\, code gen erators have been formally verified using theorem provers\, but this is ver y timeconsuming work\, should ...continue reading XALTDESC;FMTTYPE=text/html:In modeldriven development\, the automate d generation of a multithreaded program based on a model specifying the in tended system behaviour is an important step. Verifying that such a generat ion step semantically preserves the specified functionality is hard. In rel ated work\, code generators have been formally verified using theorem prove rs\, but this is very timeconsuming work\, should be done by an expert in formal verification\, and is not easily adaptable to changes applied in the generator. In this paper\, we propose\, as an alternative\, a pushbutton approach\, combining equivalence checking and code verification with previo us results we obtained on the verification of generic code constructs. To i llustrate the approach\, we consider our SLCO framework\, which contains a generator of multithreaded Java code. Although the technique can still onl y be applied to verify individual applications of the generator\, its push button nature and efficiency in practice makes it very suitable for nonexp erts.
This is joint work with Maciej Wilkowski.
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/antonwijsmodularindire ctpushbuttonformalverificationofmultithreadedcodegenerators/ END:VEVENT BEGIN:VEVENT UID:20190917T1431Z1568730668.3326EO6021@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190917T135637Z LASTMODIFIED:20190917T135637Z DTSTART;TZID=Europe/Amsterdam:20190919T124500 DTEND;TZID=Europe/Amsterdam:20190919T133000 SUMMARY: Muhammad Osama: “SIGmA: GPU Accelerated Simplification of SAT Form ulas” DESCRIPTION: In this talk\, I will present SIGmA (SAT sImplification on GPU Architectures)\, a preprocessor to accelerate SAT solving that runs on NVI DIA GPU(s). We discuss the tool\, focusing on its full functionality\, incl uding new simplifications and multiGPU support with load balancing mechani sm. SIGmA performs various types of simplification\, such as variable elimi nation\, subsumption elimination\, blocked ...continue reading XALTDESC;FMTTYPE=text/html:In this talk\, I will present SIGmA (SAT s Implification on GPU Architectures)\, a preprocessor to accelerate SAT solv ing that runs on NVIDIA GPU(s). We discuss the tool\, focusing on its full functionality\, including new simplifications and multiGPU support with lo ad balancing mechanism. SIGmA performs various types of simplification\, su ch as variable elimination\, subsumption elimination\, blocked clause elimi nation and hidden redundancy elimination. We study the effectiveness of our tool when applied prior to SAT solving. Overall\, for our large benchmark set of problems\, SIGmA enables MiniSat and Lingeling to solve many problem s in less time compared to applying the SatElite/Lingeling(integrated) prep rocessors.
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/muhammadosamasigmagpu acceleratedsimplificationofsatformulas/ END:VEVENT BEGIN:VEVENT UID:20190910T0952Z1568109155.1282EO6001@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190910T095221Z LASTMODIFIED:20190910T095221Z DTSTART;TZID=Europe/Amsterdam:20190912T124500 DTEND;TZID=Europe/Amsterdam:20190912T133000 SUMMARY: Rob van Glabbeek: Is SpeedIndependent Mutual Exclusion Implementa ble? DESCRIPTION: A mutual exclusion algorithm is called speed independent if it s correctness does not depend on the relative speed of the components. Famo us mutual exclusion protocols such as Dekker’s\, Peterson’s and Lamport’s b akery are meant to be speed independent. In this talk I argue that speedin dependent mutual exclusion may not be implementable on standard hardware\, depending ...continue reading XALTDESC;FMTTYPE=text/html:A mutual exclusion algorithm is called spe ed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's\, Peters on's and Lamport's bakery are meant to be speed independent. In this talk I argue that speedindependent mutual exclusion may not be implementable on standard hardware\, depending on how we believe reading and writing to a me mory location is really carried out. It can be implemented on electrical ci rcuits\, however. This builds on previous work showing that mutual exclusio n cannot be accurately modelled in standard process algebras.
CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/robvanglabbeekisspeed independentmutualexclusionimplementable/ END:VEVENT BEGIN:VEVENT UID:20190906T1128Z1567769339.6213EO5991@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190906T112229Z LASTMODIFIED:20190910T142059Z DTSTART;TZID=Europe/Amsterdam:20190905T124500 DTEND;TZID=Europe/Amsterdam:20190905T133000 SUMMARY: David N. Jansen: Branching bisimulation – current status DESCRIPTION: Branching bisimulation is a behavioural equivalence relation o n labelled transition systems that takes internal actions into account. Whi le it is slightly coarser than weak bisimulation\, it has the advantage tha t there is a unique branching bisimulation equivalence quotient that can be found efficiently. With m the number of transitions and n the number of st ates\, ...continue reading XALTDESC;FMTTYPE=text/html:Branching bisimulation is a behavioural eq uivalence relation on labelled transition systems that takes internal actio ns into account. While it is slightly coarser than weak bisimulation\, it h as the advantage that there is a unique branching bisimulation equivalence quotient that can be found efficiently. With m the number of transitions an d n the number of states\, the classic O(mn) algorithm has recently been re placed by an O(m log n) algorithm\, which is unfortunately rather complex. This paper provides a much more straightforward O(m log n) algorithm. Bench marks show that in practice this new algorithm is faster and more memory ef ficient than its predecessors.
(Joint work with Jan Friso Groote\, Je roen Keiren and Anton Wijs)
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/davidnjansenbranching bisimulationcurrentstatus/ END:VEVENT BEGIN:VEVENT UID:20190815T1346Z1565876794.6244EO5901@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190815T133806Z LASTMODIFIED:20190815T154213Z DTSTART;TZID=Europe/Amsterdam:20190826T150000 DTEND;TZID=Europe/Amsterdam:20190826T153000 SUMMARY: Msc presentation Johri van Eerd DESCRIPTION: Johri van Eerd will present his master thesis research on Mond ay August 26 at 15:00 in Atlas 2.215. His presentation addresses the questi on on whether term rewriting on GPUs is competitive compared to term rewrit ing on CPUs. XALTDESC;FMTTYPE=text/html:Johri van Eerd will present his master the sis research on Monday August 26 at 15:00 in Atlas 2.215. His presentation addresses the question on whether term rewriting on GPUs is competitive com pared to term rewriting on CPUs.
CATEGORIES:MSc Defence LOCATION:Atlas 2.215 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/mscpresentationjohriva neerd/ END:VEVENT BEGIN:VEVENT UID:20190812T1042Z1565606570.2564EO5871@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190812T091024Z LASTMODIFIED:20190812T091024Z DTSTART;TZID=Europe/Amsterdam:20190812T140000 DTEND;TZID=Europe/Amsterdam:20190812T144500 SUMMARY: Kevin Nogarede: An approachable language for formal requirements DESCRIPTION: Formal system verification is a mathematical technique for est ablishing whether a process meets certain design requirements. Typically\, such techniques require notation in academic languages which are difficult for engineers to write and interpret. We aim to develop a new DSL for forma lizing requirements that dramatically lowers the barrier of entry by introd ucing notation and concepts ...continue reading XALTDESC;FMTTYPE=text/html:Formal system verification is a mathematic al technique for establishing whether a process meets certain design requir ements. Typically\, such techniques require notation in academic languages which are difficult for engineers to write and interpret. We aim to develop a new DSL for formalizing requirements that dramatically lowers the barrie r of entry by introducing notation and concepts that are intuitively unders tandable yet still amenable to automated verification. The applicability of the new language is assessed via user experience reports
CATEGORIES:MSc Defence 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/kevinnogaredeanapproac hablelanguageforformalrequirements/ END:VEVENT BEGIN:VEVENT UID:20190702T1547Z1562082443.3325EO5851@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190702T132921Z LASTMODIFIED:20190702T132921Z DTSTART;TZID=Europe/Amsterdam:20190704T124500 DTEND;TZID=Europe/Amsterdam:20190704T133000 SUMMARY: David N. Jansen: Revisiting Weak Simulation for Substochastic Mark ov Chains DESCRIPTION: The spectrum of branchingtime relations for probabilistic sys tems has been investigated thoroughly by Baier\, Hermanns\, Katoen and Wolf (2003\, 2005)\, including weak simulation for systems involving substochas tic distributions. Weak simulation was proven to be sound w. r. t. the live ness fragment of the logic PCTL\\X \, and its completeness was conjectured. We revisit this result ...continue reading XALTDESC;FMTTYPE=text/html:The spectrum of branchingtime relations f or probabilistic systems has been investigated thoroughly by Baier\, Herman ns\, Katoen and Wolf (2003\, 2005)\, including weak simulation for systems involving substochastic distributions. Weak simulation was proven to be sou nd w. r. t. the liveness fragment of the logic PCTL\\X \, and its completen ess was conjectured. We revisit this result and show that soundness does no t hold in general\, but only for Markov chains without divergence. It is re futed for some systems with substochastic distributions. Moreover\, we prov ide a counterexample to completeness. In this paper\, we present a novel de finition that is sound for live PCTL\\X \, and a variant that is both sound and complete.
A joint work with Lei Song and Lijun Zhang.
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/davidnjansenrevisiting weaksimulationforsubstochasticmarkovchains/ END:VEVENT BEGIN:VEVENT UID:20190625T1629Z1561480153.017EO5841@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190625T160324Z LASTMODIFIED:20190625T160324Z DTSTART;TZID=Europe/Amsterdam:20190627T124500 DTEND;TZID=Europe/Amsterdam:20190627T133000 SUMMARY: Mark Bouwman: Formal Modelling and Verification of an Interlocking using mCRL2 DESCRIPTION: This paper presents an application of the formal modelling and model checking toolkit mCRL2 and the modelbased testing tool JTorX in the signalling domain. The mCRL2 toolkit is used to formally model the behavio ur of a system at the core of signalling solutions: the interlocking. The m odel of the interlocking is validated through modelbased testing. We ...co ntinue reading XALTDESC;FMTTYPE=text/html:This paper presents an application of the formal modelling and model checking toolkit mCRL2 and the modelbased testi ng tool JTorX in the signalling domain. The mCRL2 toolkit is used to formal ly model the behaviour of a system at the core of signalling solutions: the interlocking. The model of the interlocking is validated through modelbas ed testing. We use the mCRL2 toolkit to verify highlevel safety properties of the interlocking software.
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/markbouwmanformalmodel lingandverificationofaninterlockingusingmcrl2/ END:VEVENT BEGIN:VEVENT UID:20190625T1046Z1561459595.5976EO5821@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190625T103930Z LASTMODIFIED:20190625T103930Z DTSTART;TZID=Europe/Amsterdam:20190626T140000 DTEND;TZID=Europe/Amsterdam:20190626T143000 SUMMARY: Ruud Meeuws: Model Checking Supermodels Workbench with mCRL2 DESCRIPTION: At Sioux\, a modeldriven development tool is created. It allo ws users to create a model and generate software for specific hardware plat forms. For this tool\, Sioux wants to incorporate model checking in order t o improve the correctness and safety of software. To see whether model chec king is viable for industrial models\, we want to explore ...continue readi ng XALTDESC;FMTTYPE=text/html:At Sioux\, a modeldriven development tool
is created. It allows users to create a model and generate software for sp
ecific hardware platforms. For this tool\, Sioux wants to incorporate model
checking in order to improve the correctness and safety of software. To se
e whether model checking is viable for industrial models\, we want to explo
re the possibilities in limiting behaviour such that model checking becomes
feasible. We specify several execution models and see the influence of
them on the efficiency and feasibility of model checking with mCRL2 for t
his development tool.
Abstract: In the field of automata learnin g\, similar to modelbased testing\, a target machine is sent interrogative queries with the goal of uncovering its behaviour. The most common algorit hm for this in the industry is L*_Mealy\, a Mealymachinelearning variant of Dana Angluin's 1987 L*. In its current implementation\, no means of filt ering queries is available. In 2010\, however\, Fides Aarts and Frits Vaand rager presented a formalism that specifies certain patterns of restriction on the learner: an interface automaton they called the Learning Purpose. To gether with it\, they devised and implemented framework\, including a Mealy machine translator\, to learn interface automata\, which are similar to I/ O automata\, where the learner is restricted or rather guided through the l earning purpose automaton. In this talk\, I am going to explain their learn ing framework and focus on the learning purpose with the purpose of examini ng its expressivity in specifying desired patterns in learning\, and examin ing the possibility of extending it.
CATEGORIES:Colloquium LOCATION:MF 6.132 GEO:51.447551;5.487453 ORGANIZER;CN="Alexander Fedotov":MAILTO:a.fedotov@tue.nl URL;VALUE=URI:https://fsa.win.tue.nl/events/event/omaralzuhaibiautomatal earningwithapurpose/ END:VEVENT BEGIN:VEVENT UID:20190612T2218Z1560377918.0069EO5781@37.128.148.44 STATUS:CONFIRMED DTSTAMP:20210511T214441Z CREATED:20190612T195857Z LASTMODIFIED:20190612T195857Z DTSTART;TZID=Europe/Amsterdam:20190613T124500 DTEND;TZID=Europe/Amsterdam:20190613T133000 SUMMARY: Anton Wijs: “Check Your Locks and Fences: Integrating Model Checki ng into Fence and Transaction Insertion Analysis” DESCRIPTION: When targeting modern parallel hardware architectures\, constr ucting correct and highperforming software is complex and timeconsuming. In particular\, reorderings of memory accesses that violate intended sequen tially consistent behaviour are a major source of bugs. Applying synchronis ation mechanisms to repair these should be done sparingly\, as they negativ ely impact performance. In this work\, we propose a technique ...continue r eading XALTDESC;FMTTYPE=text/html: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:20210511T214441Z 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 means th at the complexity for LTSs actually is O(m (log n + log Act)) and in prac tice the memory requirements are ...continue 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:20210511T214441Z 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 Automated Reasoning\, over the years. These include dead lock checking in hardware and infinite branching. 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:20210511T214441Z 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 have axiomatised one of the eq uivalences\, based on weighed traces\, which is a complete axiomatisation\, to gain a better understanding ...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:20210511T214441Z 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 properties we observed that the approach is not practical. In this talk I will explain Bradfield and Stirling’s proo f system\, ...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:20210511T214441Z 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 problem whether the r emaining candidate srg(3250\,57\,0\,1) exists at all. I have developed an a lgorithm that constructs a partial solution to ...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:20210511T214441Z 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 the data type that descri bes the abstract syntax. Concrete syntax patterns allow meta programmers to create and perform matching on syntax trees using ...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:20210511T214441Z 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\, and there is insufficient documentation. This makes it very hard to make any changes\, or to add new functionality. During the ...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:20210511T214441Z 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 and yet the bottleneck for state space generation is often found in the rewriter. This calls for optimizing this part ...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:20210511T214441Z 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 on the use of logical formulas as tests\ , based on a dual adjunction between states and logical theories. This allo ws ...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:20210511T214441Z 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 have a formal semantics of the modelling language used\, which in our case is OIL (Océ Interaction Language). We show ...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:20210511T214441Z 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 specification. Previously\, Wang et al. presented an algorith m based on antichains to efficiently decide stable failures refinement and failuresdivergences refinement. ...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:20210511T214441Z 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 this verification relies on a tran slation of individual components to mCRL2\, a processalgebraic model check er. We show how to extend ...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:20210511T214441Z
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 SATproblem\, which is advantageous in terms o
f scalability. Later on\, Verbeek et al. proposed an approach to combine ba
sic xMAS ...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:20210511T214441Z 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 branching probabilistic bisimulati on. Exploiting the notion of a concrete process and building on the complet eness of strong probabilistic bisimulation\, a ...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:20210511T214441Z 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 increase of computational power of comput ers\, also opens up ways to partially automate parts of the verification pr ocess. We present ...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:20210511T214441Z 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 and successful termination it is possible to express a notion of intermediate acceptance a s it occurs\, e.g.\, in (classical) finite ...continue reading 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:20210511T214441Z 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 data structures. 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:20210511T214441Z 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 of control strategies are computat ionally hard and generally rely on the use of approximate abstractions. Bui lding on approximate abstractions\, we ...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:20210511T214441Z 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 specifies the set of formulae that are preserved and reflected by conformance. We present what is to our knowledge\, the ...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:20210511T214441Z 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 propose a new efficient parallel strategy for the ACO algorithm executed entirely on the CUDA architecture\, and perform experiments to .. .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:20210511T214441Z 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 domain specific language called SLCO that can be used to specify software behaviour. One of the features of the framewor k ...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:20210511T214441Z 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 how. 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:20210511T214441Z 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. Second\, there are several new and improved implementations of behaviou ral relations: the GJKW algorithm for branching bisimulation with complexit y O(m ...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:20210511T214441Z 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 satisfies some properties. For recursive processes thi s relation often becomes infinite and complicated\, which may lead to awkwa rd and long ...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:51.447551;5.487453 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:20210511T214441Z 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:51.447551;5.487453 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:20210511T214441Z 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:51.447925;5.484193 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:20210511T214441Z 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. In this work a Boolean network model for RA is analysed. Two kin ds of models\, synchronous and asynchronous are compared. ...continue readi ng 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:20210511T214441Z 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 in the wrong place\, our current set of tools maybe unable to solve the resul ting model checking problem. An example ...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:51.447551;5.487453 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:20210511T214441Z 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 unit: the wafer hanlder and the wafer stage. The model of such a machine is built by using the mCRL2 ...continue reading 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:20210511T214441Z 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 presentation I will summarise his recent paper titled ‘Learnin g Product Automata’ and how it relates to my work. I will ...continue readi ng 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:20210511T214441Z 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 is restricted to a small set of welldefined primitives. Rec ently\, Verbeek et al. extended this approach to state machines. In ...cont inue 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:51.447551;5.487453 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:20210511T214441Z 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 for instance learn a queue with limited size that stores arb itrary natural numbers. The conclusion is that indeed practical software .. .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:20210511T214441Z 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 whether there exist finite axiomatisations that are om egacomplete. We add termination and sequential composition to the spectrum by studying the ...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:20210511T214441Z 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 use the revised semantics for seq uential composition (TSP\;). First\, a groundcomplete axiomatisation is pr oposed for TSP\;\, extended with an auxiliary ...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:20210511T214441Z 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 of a square grid structure comp osition and analysis is presented. Parametric specification of Petri nets\, parametric representation of infinite systems ...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:20210511T214441Z 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 properties and requirements is limited to the scope of singl e components\, disallowing the verification of endtoend properties. We pr esent an ...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:20210511T214441Z 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 library facilitates the c reation and destruction of terms. In this presentation I will present sever al challenges that I encountered while ...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:20210511T214441Z 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:51.447925;5.484193 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:20210511T214441Z 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 been recorded\, each covering around 10 minutes\, by which the first MOOC on satisfiability is nearly finished. Roughly this MOO C ...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:20210511T214441Z 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 that the binomial and Poisson moment closure approx imations have the potential to accurately represent the expected behaviour of these models. ...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:20210511T214441Z 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 ongoing work towards an attempt to reap the benefits of processor arithmetic without loosing the advantages of the numbers represen ted ...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:20210511T214441Z 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 by Classen et al. we try to devise logics to fo rmally describe properties suitable for the analysis of SPLs. We ...continu e 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:20210511T214441Z 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 formal ly modelled and analysed the principles of ERTMS Hybrid Level 3 in mCRL2. O ur analysis has resulted in suggestions for ...continue 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:20210511T214441Z 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 can be utilized to perform variable and subsumption eliminations in parallel. Benchmarks show that our proposed simplifier (SI GmA) achieved an ...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:20210511T214441Z 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 a probabilistic automaton. Besides socalle d Ordered Balanced Trees\, the BEM algorithm uses straightforward datastruc tures. More recently\, Groote and Rivera Verduzco ...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:20210511T214441Z 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. It is now possible to generate counterexamples and translate them back to the original model. The first applications of this ...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:20210511T214441Z 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 this talk\, I will address complications and progr ess on my static analysis tooling in Rascal. 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:20210511T214441Z 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 in particular in the context of the recently accepted TOP project AVVA (Accelerated Veri fication and Verified Acceleration). I will present ...continue reading 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:20210511T214441Z 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 at processes using process theory and more finegrained equivale nces\, such as branching bisimulation and contrasimulation. We identify two difficulties when ...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:20210511T214441Z 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 we call model learning comes to aid. As pleasant in theory\, as perilous in application it is however. This present ation ...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:20210511T214441Z 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 of a NoC\, such as network calculus\, and low leve l simulation environments\, such as a cycleaccurate simulation of the Regi ster ...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:20210511T214441Z 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 by designers. We address the cha llenge of bridging this gap\, namely\, relating abstract specifications to RTL implementations. An important feature ...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:20210511T214441Z 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 the original model checking question. However\, for infinite systems\, such as realtime syste ms\, the parity game corresponding to most nontrivial ...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:20210511T214441Z 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 implemented. An interesting aspect is that we can model asynchrono us systems. This part still requires some research and might generate ...co ntinue 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:20210511T214441Z 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 pure propositional formulas. Next we see how the same techniques can be extended to SMT = satisfiability modulo theories\, in ...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:20210511T214441Z 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 equation systems. Solvin g parameterised boolean equation systems with realvalued parameters is not possible in most cases. We will show that ...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:20210511T214441Z 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 executions\, the system should fulfill linearizability. V erifying linearizability consists of checking that every concurrent executi on is equivalent to some sequential ...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:20210511T214441Z 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 models on the other hand often focus on a stable network\, ignoring he dynamic interactions of unstable systems. We provide ...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:20210511T214441Z 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 and only if its subterms satisfy certain formulas\, obtained by decomposing the original formula. They used this decomposition method to ...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:20210511T214441Z 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 this opportunity t o report on some progress which has been made regarding this problem: 1) It is sufficient to rewrite ...continue reading 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:20210511T214441Z 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 capabilities of Spoofax and then zoom in on its metalanguage for the specification of type systems based on scope graphs ...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:20210511T214441Z 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 a finite automaton is denoted by a regul ar expression. We extend regular expressions with a parallel construct and finite automata ...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:20210511T214441Z 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 a concurrent system tends to increase exponentially as the numb er of parallel processes increases linearly. To combat state space explosio n ...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:20210511T214441Z 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\, therefore formal verification me thods should be used to ensure correctness of these NetworksonChips. This thesis uses the MaDL modelling language ...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:20210511T214441Z 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\, I will introduce ClaiR\, a generic C++ analysis framework I built on top of the metaprogramming language Rascal. Also\, I ...continue readi ng 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:20210511T214441Z 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 this logic to practice. We attempt to find intuitive meaning for plm u*+formulas with the aim to create guidelines to create ...continue readin g 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:20210511T214441Z 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 decision by hiding some of their attributes. The extended evaluation of an ABAC policy takes such attribute hiding into account ...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:20210511T214441Z 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 component in an industrial setting at Philips Healthcare\, how I mana ged to overcome some of those challenges\, and how I ...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 BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 DTSTART:20191027T010000 TZNAME:CET END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 DTSTART:20200329T010000 TZNAME:CEST END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 DTSTART:20201025T010000 TZNAME:CET END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 DTSTART:20210328T010000 TZNAME:CEST END:DAYLIGHT END:VTIMEZONE END:VCALENDAR