|
Change #29296
2014-07-29
09:05:22
|
create
Calagator::Event
1250466729
Galois tech talk: Verifying C programs in Coq using VST
Roll back
| description |
nil |
→ |
**abstract:** C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof has the assumption that the compiler behaves exactly the way it is expected to. Verified Software Toolchain (VST) answers this problem by providing a logic specified at the source level that proves properties about generated assembly code. It is proved sound w.r.t. the operational semantics of C, the same operational semantics compiled by the proved-correct CompCert verified optimizing C compiler. Both of those proofs are machine-checked in Coq, an interactive proof assistant. This talk will present the basics of VST, followed by an example proof of a C program.
**bio:** Josiah (Joey) Dodds is an intern at Galois for the summer, researching the verification of cryptographic libraries. After the summer he will return to finish his PhD at Princeton, where he has been verifying information-flow properties and C programs in Coq. |
| end_time |
nil |
→ |
2014-08-05 12:00:00 -0700 |
| id |
nil |
→ |
1250466729 |
| start_time |
nil |
→ |
2014-08-05 11:00:00 -0700 |
| title |
nil |
→ |
Galois tech talk: Verifying C programs in Coq using VST |
| url |
nil |
→ |
http://galois.com/blog/2014/07/tech-talk-verifying-c-programs-coq-using-vst/ |
| venue_id |
nil |
→ |
202390439 |
|