[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: ddieckma@ececs.uc.edu (Darryl Scott Dieckman)*Subject*: Re: EXPAND and IF-THEN?*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Wed, 28 Jan 1998 17:36:09 -0600 (CST)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199801282126.QAA04747@clifford.ececs.uc.edu> from "Darryl Scott Dieckman" at Jan 28, 98 04:26:19 pm

> > I am attaching the PVS dump file for my theories. Within the Sane > theory, I was trying to prove the aegis_secure theorem. The partial > proof included runs find on both linux and solaris machines. However, > if after running the partial proof, you execute > (postpone) > (expand "governService") > > PVS goes off, and never comes back (never being greater than 45 > minutes). You're trying to do too much at once. You have to have define some lemmas here, doing arbitrary expansions on a state as complicated as yours gets too hard for the theorem prover to follow. We run into similar problems whenever we define multiple state transitions. Properties of these iterated functions on state (node in your case) tend to be difficult to prove. We often prove lemmas for each individual transition, and use the lemmas to get the final result. However, if you're bound and determined to proceed along this path of proving everything at once, here's the proof file for the "first" case, that avoids the evil pvs halting expansions. Note, however, that in this case, the theorem isn't true, (you end up having to show.... validCertificate = unknown which I'm assuming is false) The trick on proving complicated theorems about record updates like you have here is to work "outside in." Then when you get to a point where the field is updated, the rest of the expansions can be ignored. I've appended my first try at the proof to the mail message. If I were doing it again, I'd do it differently, but I'm getting too hungry to run through it again. Hope this helps, feel free to ask if I'm spewing smoke. John ==============================++==================== John Hoffman, PhD || Secure Computing Corporation || What do you want to 2675 Long Lake Road || read for, when you Roseville, MN 55124 || can watch TV? hoffman@securecomputing.com || Fax :(612)628-2701 || - Matilda's Father Phone:(612)628-2808 || ==============================++==================== -------------------- ("" (USE "initialAEGISServices") (FLATTEN) (SIMPLIFY) (SPLIT) (("1" (EXPAND "saneBoot") (EXPAND "getResource") (EXPAND "executeBootSequence") (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REPLACE -6) (HIDE -1 -2 -3 -4 -5 -6) (EXPAND "levelZeroBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -7) (REPLACE -1) (HIDE -1) (EXPAND "levelOneBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -8) (REPLACE -1) (HIDE -1) (EXPAND "levelTwoBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -9) (REPLACE -1) (HIDE -1) (EXPAND "levelThreeBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -10) (REPLACE -1) (HIDE -1) (EXPAND "levelFourBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -11) (REPLACE -1) (HIDE -1) (EXPAND "levelFiveBoot") (EXPAND "installAEGISResources") (EXPAND "installResource") (ASSERT) (POSTPONE)) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)) ("3" (POSTPONE)) ("4" (POSTPONE)) ("5" (POSTPONE))))

- Prev by Date:
**Re: EXPAND and IF-THEN?** - Next by Date:
**Re: EXPAND and IF-THEN?** - Prev by thread:
**Re: EXPAND and IF-THEN?** - Next by thread:
**Re: EXPAND and IF-THEN?** - Index(es):