FAST: Fast Acceleration of Symbolic Transition Systems. fast is a tool for the analysis of infinite systems. This paper describes the underlying theory, the architecture choices that have been made in the tool design. The user must provide a model to analyse, the property to check and a computation policy. Several such policies are proposed as a standard in the package, others can be added by the user. fast capabilities are compared with those of other tools. A range of case studies from the literature has been investigated

References in zbMATH (referenced in 38 articles )

Showing results 1 to 20 of 38.
Sorted by year (citations)

1 2 next

  1. Finkel, Alain; Praveen, M.: Verification of flat FIFO systems (2020)
  2. Holík, Lukáš; Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Abstraction refinement and antichains for trace inclusion of infinite state systems (2020)
  3. Boutonnet, Rémy; Halbwachs, Nicolas: Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (2018)
  4. Kukovec, Jure; Konnov, Igor; Widder, Josef: Reachability in parameterized systems: all flavors of threshold automata (2018)
  5. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  6. Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef: (\textPara^2): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms (2017)
  7. Konnov, Igor; Veith, Helmut; Widder, Josef: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability (2017)
  8. Lengál, Ondřej; Lin, Anthony W.; Majumdar, Rupak; Rümmer, Philipp: Fair termination for parameterized probabilistic concurrent systems (2017)
  9. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2016)
  10. Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  11. Bouchy, Florent; Finkel, Alain; San Pietro, Pierluigi: Dense-choice counter machines revisited (2014)
  12. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Acceleration of the abstract fixpoint computation in numerical program analysis (2012)
  13. Schrammel, Peter; Jeannet, Bertrand: Applying abstract acceleration to (co-)reachability analysis of reactive programs (2012)
  14. Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš: Programs with lists are counter automata (2011)
  15. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2011)
  16. Colón, Michael A.; Sankaranarayanan, Sriram: Generalizing the template polyhedral domain (2011)
  17. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Abstract fixpoint computations with numerical acceleration methods (2010)
  18. Bozga, Marius; Iosif, Radu; Perarnau, Swann: Quantitative separation logic and programs with lists (2010)
  19. Klaedtke, Felix: Ehrenfeucht-Fraïssé goes automatic for real addition (2010)
  20. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)

1 2 next