VeriFun

VeriFun is a reasoning system for verification of statements about programs written in a simple functional language. It was designed and developed as an easy to learn and easy to use system for teaching Automated Reasoning, Semantics, Verification and similar subjects and has been used in beginner courses about Formal Methods as well as in practical courses about Program Verification for about 15 years at the Technische Universität Darmstadt.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 10 articles , 1 standard article )

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

  1. Walther, Christoph; Wasser, Nathan: Fermat, Euler, Wilson -- three case studies in number theory (2017)
  2. Sabel, David; Schmidt-Schauß, Manfred: A two-valued logic for properties of strict functional programs allowing partial functions (2013)
  3. Leino, K. Rustan M.: Automating induction with an SMT solver (2012)
  4. Fuhs, Carsten; Giesl, Jürgen; Parting, Michael; Schneider-Kamp, Peter; Swiderski, Stephan: Proving termination by dependency pairs and inductive theorem proving (2011)
  5. Aderhold, Markus: Second-order programs with preconditions (2010)
  6. Swiderski, Stephan; Parting, Michael; Giesl, Jürgen; Fuhs, Carsten; Schneider-Kamp, Peter: Termination analysis by dependency pairs and inductive theorem proving (2009)
  7. Schlosser, Andreas; Walther, Christoph; Gonder, Michael; Aderhold, Markus: Context dependent procedures and computed types in \textttVeriFun (2007)
  8. Stump, Aron (ed.); Xi, Hongwei (ed.): Proceedings of the programming languages meets program verification (PLPV 2006), Seattle, WA, USA, August 21, 2006 (2007)
  9. Walther, Christoph; Schweitzer, Stephan: Reasoning about incompletely defined programs (2005)
  10. Yorsh, Greta; Musuvathi, Madanlal: A combination method for generating interpolants (2005)