Category archives for Uncategorized

VSCOMP 2014 Solutions

This page links to the teams and their solutions Cha-cha-cha IncreMentally Challenged ProofInUse SPARK 2014 Team KIV VerCors VeriFast Viorel Prioteasa

IncreMentally Challenged

Team: Nadia Polikarpova, Julian Tschannen, Scott West Solution 1 Solution 2 Solution 4

Xiaongmao 1

Jean-Jacques Levy, Chen Ran

SPARK 2014

Team: Johannes Kanig, Julien Thierry, Zhi Zhang Solution 1 Solution 2


Team: Bart Jacobs Solution 3 Solution 4

Team KIV

Team: Gidon Ernst, Jörg Pfähler, Bogdan Tofan Solution 1 Solution 2 Solution 4


Maria Christakis, Rustan Leino, Dan Rosen Cha-cha-cha Solution 1 Cha-cha-cha Solution 2 Cha-cha-cha Solution 4


Team: David Mentre, Claude Marche, Yannick Moy Solution 1 Solution 2


  Team: Stefan Blom, Saeed Darbari Solution 1

Xiongmao 1 Solution

Here is the solution emailed in by the team.   smallxiongmao1

Log-based set in VeriFast (partial)

logset   Very partial. Defined an abstraction relation. Defined a rely condition. Verified major part of update(). Did not verify lookup() or collect() or advance of tl, but invariant/rely condition should allow their verification. Will continue with this proof now.

Partition Refinement in KIV

An overview over the KIV project can be found here. Orange specifications in the project structure graph are imported from KIV’s library, the green specifications are problem specific additional specifications. The green color indicates that all proof obligations are done and the proofs are in a consistent state. Implementation The implementation of the algorithm can be […]

Solution for Problem 1 (ProofInUse team)

Hello, Please find our solution for problem 1, using Why3 toolset. Contact (for review): proofinuse-problem1-README proofinuse-problem1.tar All the code of our team is available on the following GitHub repository:

spark2014 – problem1

spark_problem1.tar We have successfully proved the problem 1 in Coq. In the proof for the question 1: (1) we use natural numbers to represent cards; (2) according to the concept of “precede” defined in the quetion, a(i) precedes a(j) iff i<j and a(i) < a(j), where i and j are indexes of values a(i) and […]

SPARK – problem 2

spark_problem2.tar   The attached code is an implementation of problem 2 in SPARK. However, the code does not follow the algorithm outlined in the problem description and no proof was really attempted because of lack of time to invest into the challenge. The code is annotated with executable contracts, however, which allowed to find two […]

Problem 4: Graph Cloning

This is a partial solution using some ad hoc formalisation of separation logic in Isabelle2013-2. The solution can be downloaded here: Problem4

Problem 1 – partial solution

Using our program verification (pre-processor) tool, we verified an implementation of the game that build a ghost data structure that shows that a sequence of at least as long as the number of stacks exists. problem1-sccblom.tar

IncreMentally Challenged: Problem 2

This is a partial solution to problem 2 in Dafny. Task 1: Dafny checks termination of the implementation. Task 2a: The property is added as a postcondition to the refine method. Task 2b: The predicates necessary for the verification have been defined and are checked by Dafny to be well-formed.  An informal proof sketch is […]

Solution for problem 2 (team ProofInUse)

Hi, Please find our solution for problem 2, using SPARK 2014 toolset. Contact (for review): proofinuse-problem1-README proofinuse-problem2.tar All the code of our team is available on the following GitHub repository: — Yannick Moy, Senior Software Engineer, AdaCore

Problem 3 in SPIN (team ProofInUse)

Hello,Please find attached a proposal of solution for problem 3. We have used the SPIN model checker. Contact (for review): All code of our team is available on following GitHub repository: proofinuse-problem3.tar