The modules that VeriFast automatically includes when link-checking a C program
prelude_core.h - Core of the prelude (part that is used by list.h)
list.h - Mathematical lists
prelude.h - The header file that VeriFast implicitly includes in every C file
ghost_cells.h - Auxiliary heap cells
raw_ghost_lists.h - Raw ghost lists, where each element has an id and a value
nat.h - An inductive datatype to enable natural induction on integers
listex.h - Extra definitions and lemmas about inductive datatype list
arrays.h - Useful lemmas for dealing with arrays
list.c - Implementation (i.e., proof) of the lemmas declared in list.h
raw_ghost_lists.c - Implementation of raw ghost lists in terms of ghost cells
malloc.h - Partial spec of module malloc of the C run-time library
stdio.h - Partial spec of module stdio of the C run-time library
stdlib.h - Partial spec of module stdlib of the C run-time library
string.h - Partial spec of module string of the C run-time library
threading.h - A wrapper around platform-specific threading and locking APIs; implemented by threading.c (not verified; not shown)
alt_threading.c - An alternative threading API that uses parameterized function types instead of function-pointer-indexed predicate families, plus an example of its use.
args.c - Prints the command-line arguments to the console. Shows a way to deal with arrays.
array_of_struct.c - Demonstrates how to deal with an array of struct.
barrier.c - A multithreaded program that uses a barrier for synchronization.
BeepDriver - A DLL that provides "beep" functionality and a program that uses the DLL. Demonstrates VeriFast's support for verification of unloadable modules.
libraries.h - Wrapper around the Windows/*nix DLL loading and unloading APIs. Keeps track of loaded DLLs to ensure that it always returns a freshly loaded DLL.
modules.h - Specification of a wrapper around libraries that calls an init function when the library is loaded and a dispose function when the library is unloaded. (We do not use the platform-provided library init and finalize functionality because we do not want to run code under the OS loader lock.)
modules.c - Implementation of the modules module.
BeepKernel.h - Specification of the API exposed by BeepKernel to beep drivers.
BeepKernel.c - Implementation of the beep kernel.
BeepDriver.c - An example beep driver.
BeepDriver.dlsymspec - A .dlsymspec file that associates a VeriFast contract with the function symbol exported by beep drivers. Used by the dlsymtool tool that ships with VeriFast to generate proxy .c and .h files to be used by the kernel to call the exported function symbol, and a .vfmanifest file that is used at driver link time to check that the driver does indeed export the correct function symbol with the correct contract.
BeepKernel.mysh - Command script used to verify the BeepKernel and the BeepDriver
bot.c - A chat bot (= an automated client for the chat server in chat.c)
cat.c - A verified implementation of the *nix cat command (copies a file to standard output)
char.c - An example demonstrating VeriFast's support for character literals.
chat.c - A chat server. Demonstrates the use of threads, locks, sockets, lists.
composite4.c - Demonstrates an approach for verifying instances of the Composite pattern in VeriFast. See Bart Jacobs, Jan Smans, and Frank Piessens. Verifying the Composite Pattern using Separation Logic. SAVCBS 2008 Challenge problem track.
contains.c - A collection ADT that compares elements using a user-provided equals function
contains_deep.c - A collection ADT that compares elements using a user-provided equals function; this spec facilitates compare-by-value
contrib.c - Starts two threads that share a counter and that each increment the counter; then joins both threads and asserts that the counter's value equals 2. Demonstrates shared boxes. Note: This program can be verified more simply using ghost fields. See Bart Jacobs and Frank Piessens. Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions. Technical Report CW-549, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. June 2009.
counter.c - An introductory example. A simple counter module (without abstraction) and a client program.
counter_with_pred.c - The same counter, now using abstraction.
counter_with_pred_auto.c - The same counter, now using the automatic open/close feature.
cp.c - A verified implementation of the *nix cp command (copies a file)
dyncode.c - An example that writes x86 assembly code for a plusOne function into a malloc'ed char array and then calls the function. Demonstates parameterized function types.
enums.c - An example demonstrating VeriFast's support for enums.
equalsmap.c - A collection ADT that compares elements using a user-provided equals function; alternative approach
expr.c - Builds a simple expression AST, evaluates it, and disposes it. Demonstrates a way to implement inductive datatypes in C and verify them with VeriFast.
fractions-counting.c - Shows how counting permissions can easily be integrated into VeriFast in the form of a library.
ghost_field.c - Simple ghost fields test.
globals.c - Demonstrates VeriFast's support for global variables.
goto.c - Demonstrates VeriFast's support for goto statements.
helloproc - The VeriFast Linux Kernel Module Verification Kit (under construction), and an example verified kernel module called helloproc, that implements a /proc file.
vf_README.txt - Explains the VeriFast Linux Kernel Module Verification Kit
vf_cleanup_debt.h - A VLKMVK API header file
vf_initexit.h - A VLKMVK API header file
vf_mem.h - A VLKMVK API header file
vf_mutex.h - A VLKMVK API header file
vf_printk.h - A VLKMVK API header file
vf_procfs.h - A VLKMVK API header file
helloproc_README.txt - Explains the example verified kernel module
helloproc_main.c - The example verified kernel module
ifs.c - Demonstrates how invariant statements can be used to solve the problem of exponential verification time in the presence of many independent if statements in a function.
incr_box - A program where one thread continually increments a shared counter and another reads the counter twice and asserts that the second value is not less than the first value. Demonstrates shared boxes.
incr_box.c - The program
threading.h - Specification of the threading module
threading.vfmanifest - Manifest file of the threading module
iter.c - Linked lists with iterators. There may be many iterators on a given list. Demonstrates fractional permissions and VeriFast's support for merging of fractions of precise predicates.
lcset - A concurrent set data structure implemented as a sorted linked list with hand-over-hand locking. (A more readable full proof outline of the LCSet program is shown in the appendix of CW-590.)
ghost_lists.h - Auxiliary objects that track a list; used in lcset.c to keep track of the nodes in the linked list
ghost_lists.c - Implementation of ghost lists in terms of raw ghost lists (see crt/raw_ghost_lists.h)
ghost_counters.h - Auxiliary objects that track contributions to a number; used in lcset.c to prove that when the set is disposed, no thread is holding the lock of any node
ghost_counters.c - Implementation of ghost counters in terms of raw ghost lists
atomics.h - Specification of atomic machine instructions
locks.h - Specification of the spinlocks module. A thin layer over the atomic instructions
locks.c - Implementation and proof of the spinlocks module
lcset.h - Specification of the lock-coupling set module
lcset.c - Implementation and proof of the lock-coupling set module
lcset_client.c - A client program
lemmafuncptr.c - Simple lemma function pointers test
limits.c - Demonstrates VeriFast's support for C's limits on the size of integers.
lists.h - Specification of a list module
lists.c - Implementation of the list module
map.c - Full functional specification and verification of a higher-order function: the map function known from functional programming
mcas - Full functional specification and verification of a challenging lock-free algorithm from the literature: Harris et al.'s multiple-compare-and-swap (MCAS) algorithm. The proof approach was heavily inspired by the one in Vafeiadis' PhD, but uses the approach described in CW-590 instead of rely-guarantee. (TODO: Verification of the many "trivial" lemmas used in the proof that have not yet been verified.)
bitops.h - A few lemmas about bitwise operations
atomics.h - Specification of atomic machine instructions (atomic loads and atomic (single) compare-and-swaps). You can create a "prophecy" [Abadi and Lamport] to know the value that will be read in advance. You can use a "tracked CAS" in order to predict the value that will be written by a successful CAS operation.
listex.h - Mathematical lists and "iterated star" (foreach) predicates over lists
assoc_list.h - Association lists and foreach predicates over association lists
ghost_counters.h - An auxiliary object that holds a monotonically increasing integer
ghost_lists.h - Auxiliary objects holding lists
rdcss.h - Specification of a module that implements Harris et al.'s Restricted Double Compare Single Swap algorithm, which is part of the MCAS algorithm
rdcss.c - Implementation and proof of the RDCSS algorithm
mcas.h - Specification of the MCAS module
mcas.c - Implementation and proof of the MCAS module
mcas_client.c - A minimal example client program, that uses MCAS to increment a pair of integers atomically
MockKernel - A small server that allows clients to load, unload, and use modules, similar to how operating systems allow dynamic device driver loading and unloading. Demonstrates VeriFast's support for verification of unloadable modules and programs that load and unload them.
libraries.h - A library loading/unloading API. Always returns a freshly loaded instance of the library.
MockKernel.h - The header file defining the interface between the kernel and the modules
MockKernelModule_proxy.h - The header file with the contract of the function that is dynamically looked up in the loaded DLL
MockKernel.c - The kernel
AdderModule.c - The example module
MockKernel.mysh - The command-line script for verifying the example
odd_even_lemmas.c - Demonstrates how mutual lemma recursion is possible
philosophers.c - Demonstrates VeriFast's support for deadlock prevention
queue - Full functional specification and verification of a lock-free queue implementation and an example client program. See Bart Jacobs and Frank Piessens. Modular full functional specification and verification of lock-free data structures. Technical Report CW-551, Department of Computer Science, Katholieke Universiteit Leuven, Belgium. June 2009.
atomics.h - Specification of the atomic operations library
atomics.vfmanifest - Manifest of the atomic operations library
ghost_cells.h - Specification of the ghost cells library
ghost_cells.vfmanifest - Manifest of the ghost cells library
list.h - Pure lists
queue.c - The queue implementation
queue.h - The queue specification
queue_client.c - The example client
threading.h - Specification of the threading library
threading.vfmanifest - Manifest of the threading library
sockets.h - Specification of the sockets module (a wrapper around the Win32/*nix sockets API)
sockets.vfmanifest - Manifest file for the sockets module
sorted_bintree.c - Full functional specification and verification of a binary search tree (not self-balancing)
stack.c - Example of a deep collection: a stack which owns its items. Demonstrates predicate families.
stringBuffers.h - Specification of the string buffers module
stringBuffers.c - Implementation of the string buffers module. Demonstrates the use of character arrays and strings.
swap.c - Example demonstrating the support for taking the address of a field
tuerk.c - Example demonstrating VeriFast's support for Thomas Tuerk's loop specs. (See Thomas Tuerk. Local Reasoning about While-Loops. VSTTE 2010 Theory Workshop.) A loop spec consists of a loop precondition and a loop postcondition and is an alternative to loop invariants. Loop specs enable much simpler proofs for loops that walk a recursive data structure. The loop is verified just like the corresponding tail-recursive function.
tuerk_explicit.c - A version of tuerk.c where the recursive call of the tail-recursive function is written explicitly.
wc.c - A verified implementation of the *nix wc command (counts the number of words in a given file)
See Cedric Cuypers, Bart Jacobs, and Frank Piessens. Verification of data-race-freedom of a Java chat server with VeriFast. Technical Report CW-550, Department of Computer Science, Katholieke Universiteit Leuven, Belgium.
Account.java - Demonstrates instance predicates
AraysAuto.java - Demonstrates the array handling automation
ArraysManual.java - Despite the name, demonstrates the array handling automation
chat - Java version of the chat server
Comprehensions.java - Array sum, minimum element, sorting
Constants.java - Constant fields
Contrib.java - Java version of the contrib.c example. Uses ThreadingHelper.javaspec.
Counter.java - Simple introductory example
DefaultCtor.java - Default constructor
gameserver - A multithreaded rock-paper-scissors game server
hello.scala - A tiny Scala example. Note: VeriFast's support for Scala is currently limited to essentially this example.
Iterator - A Java program consisting of multiple jar files
it.jarspec - Specification of the it module
it.jarsrc - Implementation of the it module
Iterator.java - Source file belonging to the it module implementation
Iterator.javaspec - Source file belonging to the it module specification
IteratorUtil.java - Source file belonging to the it module implementation
IteratorUtil.javaspec - Source file belonging to the it module specification
prog.jarsrc - Implementation of the prog module
Program.java - Source file belonging to the prog module implementation
SingletonIterator.java - Source file belonging to the it module implementation
SingletonIterator.javaspec - Source file belonging to the it module specification
Iterator.java - Demonstrates dynamic binding in Java
JavaCard.java - JavaCard
Map.java - Full functional specification and verification of a higher-order function: the map function known from functional programming
NestedExprTest.java - VeriFast supports nested side-effecting expressions in Java programs
Recell.java - The classic example of the power of predicate families for subtyping
Spouse.java - A non-final Person class where persons can marry and divorce. Uses fractional permissions to enforce the bidirectional binding.
Spouse2.java - A more flexible version, where subclasses do not need to use the spouse field of class Person.
SpouseFinal.java - A simple example where class Person is final
Stack.java - A simple stack
StaticFields.java - Static fields
ThreadingHelper.javaspec - Specification of a small library that enables safe joining of threads. (Thread.join is unsafe since it returns normally even if the thread being joined terminates with an exception.)
ThreadRun.java - A simplified Thread spec using instance predicates, with an example client program
Tree.java - Full functional specification and verification of binary search tree implementation (not self-balancing)