*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Symbolic execution in Isabelle.*From*: Thomas Melham <tom.melham at cs.ox.ac.uk>*Date*: Sat, 17 Apr 2021 12:35:02 +0100*Thread-topic*: Symbolic execution in Isabelle.*User-agent*: Microsoft-MacOutlook/16.47.21031401

Dear Isabelle Users, Please excuse me for a beginners’ question! My student Dapeng Gao and I are looking into using Isabelle for symbolic execution of large microprocessor instruction set specifications. Our starting point is the translation into Isabelle definitions of the SAIL specification for the CHERI RSIC-V ISA: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-risc-v.html This consists of a large number of function definitions that define the effect on visible architectural state of each of the CHERI RISC-V machine instructions – functions of the form InstructionX ins1 ins2 ... insn = <effect on an architectural state monad> where ins1, ins2, ... insn are variables raging over fields of the machine instruction X. E.g. register addresses, immediate data, etc. We want to be able to use Isabelle in “forward proof” mode, in which we specialise some or all of the variables ins1, ins2, ... insn to data structures containing some variables (for example a list of Boolean bits, each represented by a variable). And then use rewriting and simplification to compute a kind of normal form effect on machine state as a function of the inputs. I.e. get a simplified logical Is this kind of thing possible in Isabelle? We don’t want to have to type the right-and sides in, so goal directed proof is no use to us. Best regards, Tom |

**Follow-Ups**:**Re: [isabelle] Symbolic execution in Isabelle.***From:*Peter Gammie

**Re: [isabelle] Symbolic execution in Isabelle.***From:*Thomas Sewell

- Previous by Date: [isabelle] Exhaustiveness of Pure.type
- Next by Date: [isabelle] Lemma like shiftr_bl but for sshiftr in Word Library
- Previous by Thread: [isabelle] Exhaustiveness of Pure.type
- Next by Thread: Re: [isabelle] Symbolic execution in Isabelle.
- Cl-isabelle-users April 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list