COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Tests and Proofs in Isabelle

## Tests and Proofs in IsabelleAdd to your list(s) Download to your calendar using vCal - Yakoub Nemouchi, University of York
- Tuesday 10 March 2020, 14:30-14:50
- Computer Lab, SS03.
If you have a question about this talk, please contact Jean Pichon-Pharabod. Formal verification techniques have seen a remarkable boost in recent years. In particular, methods based on deductive code-verification, model-checking, and code-generation techniques can, within the boundaries of certain foundational assumptions, provide an absolute guarantee in a sense for the correctness of the components of computer based systems towards a specification. However, the assumptions underlying the model, which involves assumptions on the correctness of the compiler, hardware correctness, etc., can cause a significant gap between the specified behavior and the behavior of the code in its execution context. Thus, the verification of the underlying foundational assumptions, ie., the trusted computing base (TCB) is necessary. This can be achieved via prover based testing, where tests are generated from the verified model and executed on the verified code. During my talk, I will introduce a set of applications for this approach, namely, where two formal methods, ie., tests and proofs, are combined together on a top of the interactive theorem proving environment Isabelle. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Lab, SS03
- Computer Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsMedieval Economic and Social History Seminars Andrew Chamblin Memorial Lecture 2014 CCIMI Short Course: Random matrices, Dyson-Schwinger equations and the topological expansion## Other talksCambridge Journal of Economics 2020 Conference - postponed to 2021 Emotional Health - An Interactive Talk Babraham Distinguished Lecture - Genome regulation during developmental transitions: New views of old questions The Anne McLaren Lecture: How CST protects telomeres and double-strand breaks [POSTPONED] Languages of Emergency, Infrastructures of Response and Everyday Heroism in the Circumpolar North |