Live Verification in an Interactive Proof Assistant by Gruetter, Samuel, Fukala, Viktor, Chlipala, Adam

Get full text

Omnisemantics: Smoother Handling of Nondeterminism by Chargu?raud, Arthur, Chlipala, Adam, Erbsen, Andres, Gruetter, Samuel

Get full text

Integration verification across software and hardware for a simple embedded system by Erbsen, Andres, Gruetter, Samuel, Choi, Joonwon, Wood, Clark, Chlipala, Adam

Get full text

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs by Cao, Qinxiang, Beringer, Lennart, Gruetter, Samuel, Dodds, Josiah, Appel, Andrew W

Get full text

Flexible Instruction-Set Semantics via Abstract Monads (Experience Report) by Bourgeat, Thomas, Clester, Ian, Erbsen, Andres, Gruetter, Samuel, Singh, Pratap, Wright, Andy, Chlipala, Adam

Get full text

Foundational Integration Verification of a Cryptographic Server by Erbsen, Andres, Philipoom, Jade, Jamner, Dustin, Lin, Ashley, Gruetter, Samuel, Pit-Claudel, Clément, Chlipala, Adam

Get full text