![]() |
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 > Computer Laboratory Automated Reasoning Group Lunches > Discovery of Invariants through Automated Theory Formation
Discovery of Invariants through Automated Theory FormationAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact William Denman. Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also brings with it additional proof obligations—requiring a developer to discover properties relating to their design decisions. With the goal of reducing this burden, we have investigated how a general purpose theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. In this talk I am going to present a heuristic approach to the automatic discovery of invariants. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsCategory Theory Seminar Type the title of a new list here Cambridge Energy SeminarsOther talksDynamics of Phenotypic and Genomic Evolution in a Long-Term Experiment with E. coli Martin Roth: »Widerrede!« Big and small history in the Genizah: how necessary is the Cairo Genizah to writing the history of the Medieval Mediterranean? How to Design a 21st Century Economy - with Kate Raworth Cycles of Revolution in Ukraine |