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

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

1 2 next

  1. Boutonnet, Rémy; Halbwachs, Nicolas: Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (2018)
  2. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  3. Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef: (\textPara^2): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms (2017)
  4. Konnov, Igor; Veith, Helmut; Widder, Josef: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability (2017)
  5. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2016)
  6. Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  7. Bouchy, Florent; Finkel, Alain; San Pietro, Pierluigi: Dense-choice counter machines revisited (2014)
  8. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Acceleration of the abstract fixpoint computation in numerical program analysis (2012)
  9. Schrammel, Peter; Jeannet, Bertrand: Applying abstract acceleration to (co-)reachability analysis of reactive programs (2012)
  10. Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš: Programs with lists are counter automata (2011)
  11. Chambart, Pierre; Finkel, Alain; Schmitz, Sylvain: Forward analysis and model checking for trace bounded WSTS (2011)
  12. Colón, Michael A.; Sankaranarayanan, Sriram: Generalizing the template polyhedral domain (2011)
  13. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Abstract fixpoint computations with numerical acceleration methods (2010)
  14. Bozga, Marius; Iosif, Radu; Perarnau, Swann: Quantitative separation logic and programs with lists (2010)
  15. Klaedtke, Felix: Ehrenfeucht-Fraïssé goes automatic for real addition (2010)
  16. Kroening, Daniel; Weissenbacher, Georg: Verification and falsification of programs with loops using predicate abstraction (2010)
  17. Schrammel, Peter; Jeannet, Bertrand: Extending abstract acceleration methods to data-flow programs with numerical inputs (2010)
  18. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  19. Bouchy, Florent; Finkel, Alain; Sangnier, Arnaud: Reachability in timed counter systems (2009)
  20. Encrenaz, Emmanuelle; Finkel, Alain: Automatic verification of counter systems with ranking function (2009)

1 2 next