@inproceedings{Larsen2022,

title = {Importance Splitting in Uppaal},

author = {Kim Guldstrand Larsen and Axel Legay and Marius Mikucionis and Danny Bøgsted Poulsen},

editor = {Tiziana Margaria and Bernhard Steffen},

doi = {10.1007/978-3-031-19759-8_26},

year  = {2022},

date = {2022-11-03},

booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.

Adaptation and Learning - 11th International Symposium, ISoLA 2022,

 Rhodes, Greece, October 22-30, 2022, Proceedings, Part {III}},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{nokey,

title = {Preliminary Security Analysis, Formalisation, and Verification of  OpenTitan Secure Boot Code},

author = {Bjarke Hilmer Møler and Jacob Gosch Søndergaard and Kristoffer Skagbæk Jensen and Magnus Winkel Pedersen and Tobias Worm Bøgedal and Anton Christensen and Danny Bøgsted Poulsen and Kim Guldstrand Larsen and René Rydhof Hansen and Thomas Rosted Jensen and Heino Juvoll Madsen and Henrik Uhrenfeldt},

doi = {10.1007/978-3-030-91625-1_11},

year  = {2021},

date = {2021-10-01},

urldate = {2021-10-01},

booktitle = {Secure IT} Systems - 26th Nordic Conference, NordSec 2021, Virtual Event, November 29-30, 2021, Proceedings},

volume = {13115},

pages = {192 -- 211},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Kulczynski2021,

title = {Analysis of Source Code Using Uppaal},

author = {Mitja Kulczynski and Dirk Nowotka and Axel Legay and Danny Bøgsted Poulsen

},

doi = {10.4204/EPTCS.338.5},

year  = {2021},

date = {2021-04-19},

urldate = {2021-04-19},

booktitle = {Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24-25th May 2021},

volume = {338},

pages = {31 -- 38},

keywords = {},

pubstate = {forthcoming},

tppubtype = {inproceedings}

}

@inproceedings{Jensen2020b,

title = {Fluid Model-Checking in UPPAAL for Covid-19},

author = {Peter Gjøl Jensen and Kenneth Yrke Jørgensen and Kim Guldstrand Larsen and Marius Mikučionis and Marco Antonio Muniz Rodriguez and Danny Bøgsted Poulsen},

editor = {Tiziana Margaria and  Bernhard Steffen},

doi = {10.1007/978-3-030-61362-4_22},

year  = {2020},

date = {2020-10-31},

urldate = {2020-10-31},

booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I},

volume = {12476},

pages = {385 -- 403},

publisher = {Spring},

abstract = {During the spring of 2020, the BEOCOVID project has been funded to investigate the use of stochastic hybrid models, statistical model checking and machine learning to anlyse, predict and control the rapid spreading of Covid-19. In this paper we focus on the SEIHR epidemiological model instance of Covid-19 pandemics and show how the risk of viral exposure, the impact of super-spreader events as well as other scenarios can be modelled, estimated and controlled using the tool Uppaal SMC.},

keywords = {},

pubstate = {forthcoming},

tppubtype = {inproceedings}

}

@inproceedings{Day2020,

title = {Rule-based Word Equation Solving},

author = {Joel D. Day and Mitja Kulczynski and Florin Manea and Dirk Nowotka and Danny Bøgsted Poulsen },

url = {https://youtu.be/RwMH7h9cWwM},

doi = {10.1145/3372020.3391556},

year  = {2020},

date = {2020-10-01},

booktitle = {FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020},

pages = {87--97},

publisher = {ACM},

abstract = {We present a transformation-system-based technique in the frame-work of string solving, by reformulating a classical combinatorics on words result, the Lemma of Levi. We further enrich the induced rules by simplification steps based on results from the combinatorial theory of word equations, as well as by the addition of linear length constraints. This transformation-system approach cannot solve all equations efficiently by itself. To improve the efficiency of our transformation-system approach we integrate existing successful string solvers, which are called based on several heuristics. The experimental evaluation we performed shows that integrating our technique as an inprocessing step improves in general the performance of existing solvers.},

note = {Best Video Presentation Award },

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Kulczynski2020,

title = {The Power of String Solving: Simplicity of Comparison},

author = {Mitja Kulczynski and Florin Manea and Dirk Nowotka and Danny Bøgsted Poulsen},

doi = {10.1145/3387903.3389317},

isbn = {9781450379571},

year  = {2020},

date = {2020-03-17},

booktitle = {AST@ICSE 2020: {IEEE/ACM} 1st International Conference on Automation of Software Test, Seoul, Republic of Korea, 15-16 July, 2020},

pages = {85--88},

publisher = {ACM},

abstract = {The increased interest in string solving in the recent years has made it very hard to identify the right tool to address a particular user's purpose. Firstly, there is a multitude of string solving, each addressing essentially some subset of the general problem. Generally, the addressed fragments are relevant and well motivated, but the lack of comparisons between the existing tools on an equal set of benchmarks, cannot go unnoticed, especially as a common framework to compare solvers seems to be missing. In this paper we gather a set of relevant benchmarks and introduce our new benchmarking framework ZaligVinder to address this purpose.},

note = {Special Recognition Award (Short Paper)},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Kulczynski2019,

title = {On collapsing prefix normal words},

author = {Mitja Kulczynski and Dirk Nowotka and Pamela Fleischman and Danny Bøgsted Poulsen},

editor = {Alberto Leporati andCarlos Martín-Vide and Dana Shapira and Claudio Zandron},

doi = {10.1007/978-3-030-40608-0_29},

isbn = {978-3-030-40607-3},

year  = {2020},

date = {2020-02-25},

booktitle = {Language and Automata Theory and Applications. },

pages = {412-424},

publisher = {Springer},

series = {LNCS},

abstract = {Prefix normal words are binary words in which each prefix has at least the same number of 1s as any factor of the same length. Firstly introduced in 2011, the problem of determining the index (amount of equivalence classes for a given word length) of the prefix normal equivalence relation is still open. In this paper, we investigate two aspects of the problem, namely prefix normal palindromes and so-called collapsing words (extending the notion of critical words). We prove characterizations for both the palindromes and the collapsing words and show their connection. Based on this, we show that still open problems regarding prefix normal words can be split into certain subproblems.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Day2019,

title = {On Solving Word Equations Using SAT},

author = {Joel Day and Thorsten Ehlers and Mitja Kulczynski and Florin Manea and Dirk Nowotka and Danny Bøgsted Poulsen

},

doi = {10.1007/978-3-030-30806-3_8},

isbn = {978-3-030-30805-6},

year  = {2019},

date = {2019-09-11},

booktitle = {13th International Conference on Reachability Problems},

volume = {11674},

pages = {93--106},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

abstract = {We present Woorpje, a string solver for bounded word equations (i.e., equations where the length of each variable is upper bounded by a given integer). Our algorithm works by reformulating the satisfiability of bounded word equations as a reachability problem for nondeterministic finite automata, and then carefully encoding this as a propositional satisfiability problem, which we then solve using the well-known Glucose SAT-solver. This approach has the advantage of allowing for the natural inclusion of additional linear length constraints.

Our solver obtains reliable and competitive results and, remarkably, discovered several cases where state-of-the-art solvers exhibit a faulty behaviour.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Legay2018,

title = {Statistical Model Checking of LLVM Code},

author = {Axel Legay and Dirk Nowotka and Danny Bøgsted Poulsen and Louis-Marie Traonouez },

doi = {10.1007/978-3-319-95582-7_32},

isbn = {978-3-319-95582-7},

year  = {2018},

date = {2018-07-12},

abstract = {We present the new tool Lodin for statistical model checking of

LLVM-bitcode.  Lodin implememts a simulation engine for LLVM-bitcode

and implements classic statistical model checking algorithms on top

it. The simulation engine implements only the core of LLVM but

supports extending this core through a plugin-architecture. Besides

the statistical model checking algorithms Lodin also provides an

interactive simulation front-end. The simulator front-end was integral

for our second contribution - an integration of Lodin into

Plasma-Lab. The integration with Plasma-Lab is integral to allow

reasoning about rare properties of programs.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Li2017,

title = {Practical Controller Synthesis for MTL},

author = {Guangyuan Li and Peter Gjøl Jensen and Kim Guldstrand Larsen and Axel Legay and Danny Bøgsted Poulsen},

doi = {10.1145/3092282.3092303},

isbn = {978-1-4503-5077-8 },

year  = {2017},

date = {2017-08-01},

abstract = {Metric Temporal Logic MTL$_{0,infty}$ is  a timed extension of linear

temporal logic, LTL, with time intervals whose left endpoints are zero

or whose right endpoints are  infinity. Whereas the satisfiability and

model-checking problems  for MTL$_{0,infty}$  are both  decidable, we

note  that the  controller synthesis  problem for  MTL$_{0,infty}$ is

unfortunately  undecidable.   As  a  remedy  of  this  we  propose  an

approximate method to  the synthesis problem, which  we demonstrate to

be adequate and scalable to practical examples. We define a method for 

converting MTL$_{0,infty}$ formulas into (nondeterministic) 

Timed Game Büchi Automata and furthermore show how to construct 

determinized over- and underapproximation of a such.

For the proposed method, we present a toolchain 

seamlessly integrating the needed components for practical 

MTL$_{0,infty}$ synthesis.

Lastly we demonstrate on a pair of case-studies the applicability and scalability

of the proposed method.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Jensen2017,

title = {Quantitative Evaluation of Attack Defense Trees Using Stochastic Timed Automata},

author = {Renè Rydhof Hansen and Peter Gjøl Jensen and Kim Guldstrand Larsen and Axel Legay and Danny Bøgsted Poulsen},

doi = {https://doi.org/10.1007/978-3-319-74860-3_5},

year  = {2017},

date = {2017-08-01},

abstract = {Security analysis is without doubt one of the most important issues in  a

society relying  heavily on computer infrastructure. Unfortunately

security analysis is also very difficult due to the complexity of

systems. This is bad enough when dealing with ones own computer

systems - but nowadays organisations rely on third-party services

- cloud services -  along with their own antiquated legacy

systems. Combined this makes it overwhelming difficult to 

obtain an overview of possible attack scenarios. Luckily, some

formalisms such as attack trees exists that can help security

analysts.  However,  temporal behaviour of the attacker is rarely

considered by these formalisms.



In this paper we build upon previous work on attack-defence trees to

build a proper temporal semantics. We consider the attack-defence tree a reachability

objective for an attacker and thereby separates the attacker logic

from the attack-defence tree. We give a temporal stochastic semantics for arbitrary

attackers (adhering to certain requirements to make the attacker

``sane'') and we allow annotating attacker actions with time-dependent

costs. Furthermore, we define what we call a cost-preserving attacker

profile and we define a parameterised  attacker profile. 

The defined semantics is implemented via a translation to

Uppaalsmc. 

Using Uppaalsmc we answers various questions such as the expected

cost of an attack, we find the probability of a successful attack and

we even show how an attacker can find a optimal parameter setting

using ANOVA and Tukeys test. },

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Gadyatskaya2016,

title = {Modelling Attack-defense Trees Using Timed Automata},

author = {Olga Gadyatskaya and René Rydhof Hansen and Kim Guldstrand Larsen and Axel Legay and Mads Chr. Olesen and Danny Bøgsted Poulsen},

doi = {10.1007/978-3-319-44878-7_3},

isbn = {978-3-319-44878-7},

year  = {2016},

date = {2016-09-01},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Jegourel2016,

title = {Importance Sampling for Stochastic Timed Automata},

author = {Cyrille Jegourel and Kim Guldstrand Larsen and Axel Legay and Marius Mikucionis and Danny Bøgsted Poulsen and Sean Sedwards},

doi = {10.1007/978-3-319-47677-3_11},

isbn = {978-3-319-47677-3},

year  = {2016},

date = {2016-08-01},

abstract = {We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata.

By means of symbolic exploration, our framework first identifies states that cannot reach the goal.

A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached.

The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{David2013,

title = {Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata.},

author = {Alexandre David and Kim Guldstrand Larsen and Axel Legay and Danny Bøgsted Poulsen},

doi = {10.14279/tuj.eceasst.66.893},

year  = {2013},

date = {2013-08-01},

abstract = {In this paper  we present a modelling formalism for  dynamic networks of

stochastic hybrid automata.  In particular,  our formalism is based on

primitives for the dynamic creation and termination of hybrid automata

components during the execution of a system.  In this way we allow for

natural  modelling of concepts  such as multiple threads  found in

various programming  paradigms, as  well as  the dynamic  evolution of

biological systems.  



We provide  a natural stochastic  semantics of the  modelling formalism

based on repeated output races between the dynamic evolving components

of  a  system.  As  specification  language  we present  a  quantified

extension of the logic MTL.  

 As a main contribution of this paper, the statistical

model checking  engine of Uppaal has  been extended to the  setting of

dynamic  networks   of  hybrid   systems  and  quantified   MTL.   We

demonstrate the usefulness  of the extended formalisms  in an analysis

of a dynamic version of the  well-known Train Gate example, as well as

in natural monitoring  of a MTL formula, where  observations may lead

to dynamic creation of monitors for sub-formulas.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{David2012,

title = {Statistical Model Checking for Stochastic Hybrid Systems},

author = {Alexandre David and Dehui Du and Kim Guldstrand Larsen and Axel Legay and Marius Mikucionis and Danny Bøgsted Poulsen and Sean Sedwards},

doi = {10.4204/EPTCS.92.9},

year  = {2012},

date = {2012-08-01},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Bulychev2012,

title = {UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata.},

author = {Peter E. Bulychev and Alexandre David and Kim Guldstrand Larsen and Marius Mikucionis and Danny Bøgsted Poulsen and Axel Legay and Zheng Wang},

doi = {10.4204/EPTCS.85.1},

year  = {2012},

date = {2012-08-01},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Bulycheve2012,

title = {Rewrite-Based Statistical Model Checking of WMTL.},

author = {Peter E. Bulychev and Alexandre David and Kim Guldstrand Larsen and Axel Legay and Guangyuan Li and Danny Bøgsted Poulsen},

doi = {10.1007/978-3-642-35632-2_25},

isbn = {978-3-642-35632-2},

year  = {2012},

date = {2012-08-01},

abstract = {We present a new technique for verifying Weighted Metric Temporal

Logic (WMTL) properties of Weighted Timed Automata. Our approach

relies on Statistical Model Checking combined with a new monitoring

algorithm based on rewriting rules. Contrary to existing monitoring

approaches for WMTL ours is exact. The technique has been implemented in the

statistical model checking engine of uppaal and experiments indicate

that the technique performs faster than existing approaches and leads

to more accurate results.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{PBulychev2012,

title = {Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic.},

author = {Peter E. Bulychev and Alexandre David and Kim Guldstrand Larsen and Axel Legay and Guangyuan Li and Danny Bøgsted Poulsen and Amélie Stainer},

doi = {10.1007/978-3-642-28717-6_15},

isbn = {978-3-642-28717-6},

year  = {2012},

date = {2012-08-01},

abstract = {  We present  a  novel  approach  and  implementation  for  analysing

  WTA with  respect to  WMTL.  Based  on a stochastic  semantics of

  WTA, we apply SMC to estimate and test

  probabilities  of satisfaction  with desired  levels  of confidence.

  Our approach  consists in  generation of deterministic  monitors for

  formulae  in WMTL,  allowing  for efficient  SMC by  run-time

  evaluation  of a given  formula.  By  necessity,  the deterministic

  observers    are    in     general    approximate    (over-    or

  under-approximations), but  are most often  exact and experimentally

  tight. The technique is implemented in the new tool glitool that we

  seamlessly connect to Uppaalsmc in a tool chain.  We demonstrate the

  applicability   of  our   technique  and   the  efficiency   of  our

  implementation through a number of case-studies.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{David20122,

title = {Runtime Verification of Biological Systems.},

author = {Alexandre David and Kim Guldstrand Larsen and Axel Legay and Marius Mikucionis and Danny Bøgsted Poulsen and Sean Sedwards},

doi = {10.1007/978-3-642-34026-0_29},

isbn = {978-3-642-34026-0},

year  = {2012},

date = {2012-08-01},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{David2011,

title = {Statistical Model Checking for Networks of Priced Timed Automata},

author = {Alexandre David and Kim Guldstrand Larsen and Axel Legay and Marius Mikucionis and Danny Bøgsted Poulsen and Jonas van Vliet and Zheng Wang},

doi = {doi.org/10.1007/978-3-642-24310-3_7},

isbn = {978-3-642-24310-3},

year  = {2011},

date = {2011-08-01},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}