SG
Sylvia Grewe
Authored
5 records found
Automating Proof Steps of Progress Proofs
Comparing Vampire and Dafny
Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas [3] project aims at providing support for the development of soundness proofs of type systems and eff
...
System Description
An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers
Computer science has seen much progress in the area of automated verification in the last decades. Yet, there are many domains where abstract strategies for verifying standard properties are well-understood by domain experts, but still not automated to a satisfactory degree. One
...
System Description
An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers
Computer science has seen much progress in the area of automated verification in the last decades. Yet, there are many domains where abstract strategies for verifying standard properties are well-understood by domain experts, but still not automated to a satisfactory degree. One
...
Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we
...
Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we
...