Name	Name	Last commit message	Last commit date
parent directory ..
README.md	README.md
agc.c2po	agc.c2po
agc.csv	agc.csv
arrays.c2po	arrays.c2po
arrays.csv	arrays.csv
cav.c2po	cav.c2po
cav.csv	cav.csv
cav.map	cav.map
event.c2po	event.c2po
event.csv	event.csv
event.map	event.map
run_examples.sh	run_examples.sh
set_agg.c2po	set_agg.c2po
set_agg.csv	set_agg.csv
simple.c2po	simple.c2po
simple.csv	simple.csv
simple.map	simple.map
struct.c2po	struct.c2po
struct.csv	struct.csv

Name

Last commit message

Last commit date

Examples

To run all examples in this directory, run ./run_examples.sh.

Each of the following cases shows a minimal example of a feature discussed in the CAV 2023 paper in the indicated section:

agc Assume-Guarantee Contract: tri-state status output (inactive, invalid, or verified)
arrays Array Types: Use of parametrized typing on a structure member
cav CAV: The example from the paper showcasing a realistic composition of the other features
cse Common Subexpression Elimination: Removal of redundant work from specification
set_agg Set Aggregation: Specifications beyond binary inputs
simple Simple: A basic R2U2 V2 style specification in the V3 input language
struct Structure: Use of a structure to group variables

Provide feedback