One Day Workshop Around SMT Solvers for ProofInUse Kickoff

by Yannick Moy in Events – December 15, 2014

SMT solvers are at the heart of the automation and interaction capabilities of the new SPARK technology, with Why3 serving as intermediary. One of the challenges of the joint lab ProofInUse between Inria and AdaCore is to exploit best the capabilities of SMT solvers. Thus, we have invited developers of the Alt-Ergo and CVC4 SMT solvers, that are both distributed with current versions of SPARK, for a one-day workshop on SMT solvers. Registration if free but mandatory to attend the event, see the page of the event for the program and registration:

http://www.spark-2014.org/proofinuse/kickoff

 

 

 

 

 

 

comments powered by Disqus