List of challenges

List of challenges

The following table collects the challenges added to the EuroProofNet Program Verification inventory.

Please click on the challenge name for its detailed profile (if available) or contribute with yours.

Explanation of "Status":

• identified: the challenge has been identified, but currently there is no (known) team working on it
• active: there is someone already working on it (work in progress)
• finished: the team(s) that worked on it consider(s) that the goal has been achieved
• discontinued: the team(s) involved in the challenge do(es) not work on it anymore

Challenges

Name	Team / Community	Key aspects	Status
Attested TLS	IETF, IRTF, CCC, GA4GH, GENXT, ...	Symbolic security analysis	Active
Proof scores	FADoSS, Ogata lab	Interactive theorem proving	Active
Reasoning with laws	Barcelona Group on Pure and Applied Proof Theory	Natural language, logic, proofs, AI	Active
IA integration	FADoSS	Maude specifications; Dafny proofs	Active

Research oriented challenges

We provide here pointers to other websites describing verification challenges

• POPLmark Reloaded: How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine checked proofs?
• The Concurrent Calculi Formalisation Benchmark: propose a new collection of benchmark challenges focused on the difficulties that typically arise when mechanising formal models of concurrent and distributed programming languages
• VerifyThis Competition: series of program verification competitions, which has taken place annually since 2011. https://github.com/verifythis/verifythis.github.io
• concurrency-challenge-problem on SMTs

Industry related challenges

• Security Challenges
• Ethereum Smart Contracts challenges (and more)