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

# Category archives for **Uncategorized**

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

Jean-Jacques Levy, Chen Ran

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

Team: Bart Jacobs Solution 3 Solution 4

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: Viorel Prioteasa Solution 2 Solution 4

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

Team: Stefan Blom, Saeed Darbari Solution 1

Cha-cha-cha solution 4 is at http://rise4fun.com/Dafny/NHaHp

Cha-cha-cha solution 2 is at http://rise4fun.com/Dafny/3WDvO

This is a compete solution to Problem 1 in Dafny (but not cleaned up and not commented due to time limits). problem1

Here is the solution emailed in by the team. smallxiongmao1

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.

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 […]

Hello, Please find our solution for problem 1, using Why3 toolset. Contact (for review): Claude.Marche@inria.fr proofinuse-problem1-README proofinuse-problem1.tar All the code of our team is available on the following GitHub repository: https://github.com/yannickmoy/vscomp_2014_proofinuse

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_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 […]

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

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

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 […]

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

Hello,Please find attached a proposal of solution for problem 3. We have used the SPIN model checker. Contact (for review): dmentre@linux-france.org All code of our team is available on following GitHub repository: https://github.com/yannickmoy/vscomp_2014_proofinuse proofinuse-problem3.tar