University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Proving recursive programs terminating

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

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

ℹī¸ Information

Proving recursive programs terminating

Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk .

This talk will show that termination proving for recursive programs can be divided into two parts: the analysis of recursive programs for safety properties, and termination proving for non-recursive programs. We then show how existing tools (e.g. RHS for the analysis of recursive programs, and the TERMINATOR termination prover) can be combined into a powerful new termination prover for recursive procedures.

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 lists

Demo Room One, Demo Building Baker Building - Board Room, Department of Engineering / Online (Zoom Meeting ID: 856 0420 7880 Passcode: 578888) Institute of Metabolic Science (IMS), Level 4 ATC, Seminar rooms 1,2 & 3

Other talks

Reachability Types, Traces, and Full Abstraction CodeScaler: Scaling Code LLM Training and Test-Time Inference via Execution-Free Reward Models Title TBC Professor Philip Rosenstiel, W3 Professor of Clinical Molecular Biology, Director, Institute of Clinical Molecular Biology (IKMB), Kiel University Morning Break Precarity and the economy of makeshifts: A novel argument from the census of England, 1851-1911
 

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