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) > Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction

## Backward Analysis via Over-Approximate Abstraction and Under-Approximate SubtractionAdd to your list(s) Download to your calendar using vCal - Alexey Bakhirkin, MSR/University of Leicester
- Friday 22 August 2014, 16:00-17:00
- Room FW26, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Jonathan Hayman. We propose a novel approach for computing weakest liberal safe preconditions of programs. The standard approaches, which call for either under-approximation of a greatest fixed point, or complementation of a least fixed point, are often difficult to apply successfully. Our approach relies on a different decomposition of the weakest precondition of loops. We exchange the greatest fixed point for the computation of a least fixed point above a recurrent set, instead of the bottom element. Convergence is achieved using over-approximation, while in order to maintain soundness we use an under-approximating logical subtraction operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not restricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3-valued structures. 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 Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsLeverhulme Lecture CBL important Peterhouse Theory Group Cyber Security Society talks Engineering Design Centre Seminars Cambridge Linguistics Forum## Other talksEthics for the working mathematician, seminar 12: Going back to the start. Positive definite kernels for deterministic and stochastic approximations of (invariant) functions CANCELLED: How and why the growth and biomass varies across the tropics Childhood adversity and chronic disease: risks, mechanisms and resilience The role of Birkeland currents in the Dungey cycle Fukushima and the Law |