University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

CRUK cafe, Li Ka Shing Centre, CB2 0RE. Engineering Structures Seminar Series GR 06/07, Faculty of English

Other talks

Theophilus Richmond’s The First Crossing: The Transition from Slavery to Indentureship in the Caribbean and the Case of the Black Slave on the Hesperus Title TBC Discussion II continued Title tbc Director's Welcome Discovery Investigations: Science, Empire and the Making of the British South Atlantic
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity