Group colloquium

About model and code verificationI will use this colloquium to present what I have been doing and learning during these three initial months at FMT. You will see that there is more learning than doing, this may hopefully have to do with me jumping from my former topic: Stochastic Automata for model checking, to my current topic which is static verification of code using VerCors. I will start showing you a little bit about how VerCors works, thus we may look into separation logic for this. Afterwards, I plan to show you what we try to do with Vercors, and for this, I may go through some examples of application and talk to you about my future work directions.
Thu 24 Oct 2019 15:45 - 16:30Ravelijn - 2501
Conferences & SymposiaRead more
Simulating limit-deterministic Büchi automata for probabilistic model checkingOmega-regular languages provide a rich formalism to unambiguously express safety and progress requirements of stochastic models such as Markov decision processes (MDPs). The most common way to describe an ω-regular language is via a formula in Linear Time Logic (LTL). A typical requirement that is naturally expressed as an ω-regular objective prescribes that an agent should eventually control the MDP to stay within a given set of states, while at all times avoiding another set of states. In LTL, this would be written "(FG goal) ∧ (G ¬trap)", where "goal" and "trap" are labels attached to the appropriate states, "F" stands for "finally," and "G" stands for "globally."
Thu 7 Nov 2019 15:45 - 16:30Ravelijn - 2237
Conferences & SymposiaRead more