University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Bit-blasting in HOL4

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

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

Bit-blasting in HOL4

Add to your list(s) Download to your calendar using vCal

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

This talk describes a new LCF -style implementation of “bit-blasting”, which allows HOL4 users to automatically verify a wide range of bit-vector goals.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Type the title of a new list here 2017 Mathematics and Machine Learning

Other talks

Lunchtime Talk: Helen's Bedroom Description: TIE proteins: chemical harpoons of Gram-positive bacteria Emma Hart: Remaking the Public Good in the American Marketplace during the Early Republic Beacon Salon # 8 The Dawn of the Antibiotic Age Research frontiers and new therapeutic strategies in pancreatic cancer Nonstationary Gaussian process emulators with covariance mixtures Crowding and the disruptive effect of clutter throughout the visual system Throwing light on organocatalysis: new opportunities in enantioselective synthesis Black and British Migration DataFlow SuperComputing for BigData Cambridge Rare Disease Summit 2017
 

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