Welcome

VerifyThis is a collection of problems (and solutions) in formal verification of object-oriented (and not only) software. This collection originated in the context of the COST Action IC0701, but it is explicitly open to anyone interested in the subject. The website is in beta, so expect some rough edges.

Contact details, how to submit, and other questions answered here.

Below you see a ranked list of all entries.

You are not logged in.

You can only view existing entries. To create new entries, add solutions, edit or rate entries please login (email us to register for an account)

Sort by:  Rank  |  Alpha  |  Date

1
Binary Search in an Array

1
Sum and Maximum

1
Inverting an Injection

1
Searching a Linked List

1
N Queens

1
Amortized Queue

0
Thread-safety of java.lang.StringBuffer

0
Extracting positive elements of an array

0
Morgan's Calculator

0
The bakery protocol

0
Selection sort

0
Adding and Multiplying Numbers

0
Sorting a Queue

0
Subject-Observer Pattern

0
Database system for managing exams

0
Layered Implementation of a Map ADT

0
Linked-List Implementation of a Queue ADT

0
Iterators

0
Composite Pattern

0
Database Library

0
Modeling Types

0
Quantifiers and Comprehensions

0
Modification of Static Fields

0
Method Calls in Specifications

0
Class Initialization

0
Invariants of Complex Object Structures

0
Finalizers

0
Methods that Use Function Objects

0
Invocations of Function Objects

0
Java Machine Readable Travel Documents

0
JMM: Safe one-time publication

0
Dutch Election Software

0
Dijkstra's Shortest Path Algorithm

0
The Mobius Demonstrator Case Study

0
Red-black Tree

0
Composite Pattern 2

0
Binary Heap

0
Union Find

0
Constant Time Sparse Array

0
Maximum in an array (by elimination)

0
Maximum in a tree

0
Two equal elements

0
Cyclic list