Getting Started
Installation Guide
Tutorial
Issue Tracker
Tools
Verifier
Alpinist
VeSUV
VeyMont
Showcases
Publications
About
VerCors Team
News
Contact
Credits
License
Refute: unsatisfiable
Simple verification example of a method with a precondition that is unsatisfiable.
General Information
Backend
: Silicon
Language
: Java
Features
:
Path to Example File
: refute/Unsat.java
Should Verify
: Yes
Date
: 2017-06-20
Lines of Code
: 7 (comments not included)
Lines of Specification
: 3 (42.9% of total)
Computation Time
: 17.8 seconds
// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases RefuteUnsat //:: tools silicon //:: verdict Fail /* The pre-condition is unsatisfiable. */ public class Unsat { /*@ requires 1==0; @*/ public void bad(){ } }
Language:
PVL
Java
Cuda
C / OpenMP / OpenCL
Viper