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