Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

README.md: Documentation fixes #49

Merged
merged 4 commits into from
Feb 19, 2024
Merged

README.md: Documentation fixes #49

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
42677d2
README.md: Add CI and Hackage badges
RyanGlScott Feb 19, 2024
f1f19ff
copilot-verifier.cabal: Fix hyperlinks
RyanGlScott Feb 19, 2024
fc37af0
README.md: Wordsmithing
RyanGlScott Feb 19, 2024
b8ef4c1
README.md: Mention ICFP 2024 paper
RyanGlScott Feb 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 10 additions & 4 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
[![Build Status](https://github.com/Copilot-Language/copilot-verifier/workflows/copilot-verifier/badge.svg)](https://github.com/Copilot-Language/copilot-verifier/actions?query=workflow%3Acopilot-verifier)
[![Version on Hackage](https://img.shields.io/hackage/v/copilot-verifier.svg)](https://hackage.haskell.org/package/copilot-verifier)

# Copilot Verifier

This "Copilot Verifier" is an add-on to the
[Copilot Stream DSL](https://copilot-language.github.io)
for verifying the correctness of C code generated
by the `copilot-c99` package.
Copilot Verifier is an add-on to the [Copilot Stream
DSL](https://copilot-language.github.io) for verifying the correctness of C
code generated by the `copilot-c99` package.

The main idea of the verifier is to use the
[Crucible symbolic simulator](https://github.com/galoisinc/crucible)
Expand All @@ -15,6 +17,10 @@ verification conditions are then dispatched to SMT solvers to
be automatically solved. We will have more to say about exactly
what is meant by this correspondence below.

Copilot Verifier is described in the ICFP 2024 paper [_Trustworthy Runtime
Verification via Bisimulation (Experience
Report)_](https://dl.acm.org/doi/abs/10.1145/3607841).

## Building

To build the verifier from source, first make sure you have met the following
Expand Down
19 changes: 10 additions & 9 deletions copilot-verifier/copilot-verifier.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,17 @@ Build-type: Simple
Category: Language
Synopsis: System for verifying the correctness of generated Copilot programs
Description:
@copilot-verifier@ is an add-on to the <https://copilot-language.github.io
Copilot Stream DSL> for verifying the correctness of C code generated by the
@copilot-c99@ package.
@copilot-verifier@ is an add-on to the [Copilot Stream
DSL](https://copilot-language.github.io) for verifying the correctness of C
code generated by the @copilot-c99@ package.
.
@copilot-verifier@ uses the <https://github.com/galoisinc/crucible Crucible
symbolic simulator> to interpret the semantics of the generated C program and
and to produce verification conditions sufficient to guarantee that the
meaning of the generated program corresponds in a precise way to the meaning
of the original stream specification. The generated verification conditions
are then dispatched to SMT solvers to be automatically solved.
@copilot-verifier@ uses the [Crucible symbolic
simulator](https://github.com/galoisinc/crucible) to interpret the semantics
of the generated C program and and to produce verification conditions
sufficient to guarantee that the meaning of the generated program corresponds
in a precise way to the meaning of the original stream specification. The
generated verification conditions are then dispatched to SMT solvers to be
automatically solved.
extra-doc-files: CHANGELOG.md, README.md

source-repository head
Expand Down
Loading