FAST

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 41 articles )

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

1 2 3 next

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

1 2 3 next