WiSE.relations

WiSE.equalities

• Types With Equalities

WiSE.utils

WiSE.streams

• A library to manipulate infinite streams
  • Predicates Over Streams
  • Examples

WiSE.lang.imp

• IMP, A toy imperative programming language
  • Syntax
  • Semantics
  • Progression and Erroneous States

WiSE.lang.imprec

• IMPREC, An extension of IMP with procedures and recursion
  • Syntax
  • Semantics

WiSE.symbolic.symex

• Simple Symbolic Execution for IMP
  • Symbolic Evaluation
  • Symbolic Semantics

WiSE.symbolic.solver

• A Naive Constraint Solver/simplifier

WiSE.implem.bugfinder

• Implementation of a naive bug finder for IMP

WiSE.implem.bugfinder_proof

• Correctness proof of the bugfinder
  • Soundness and Completness of expand w.r.t sym_step
  • Eager model of run
  • LTL Specification Predicates
  • Soundess of run
  • Completeness of run

extract