SIMPAL: A Compositional Reasoning Framework for Imperative Programs

dc.contributor.advisor Ratnesh Kumar
dc.contributor.author Wagner, Lucas
dc.contributor.department Electrical and Computer Engineering
dc.date 2018-08-11T16:01:15.000
dc.date.accessioned 2020-06-30T03:09:52Z
dc.date.available 2020-06-30T03:09:52Z
dc.date.copyright Sun Jan 01 00:00:00 UTC 2017
dc.date.embargo 2018-03-06
dc.date.issued 2017-01-01
dc.description.abstract <p>The Static IMPerative AnaLyzer (SIMPAL) is a tool for performing compositional reasoning over software programs that utilize preexisting software components. SIMPAL features a specification language, called Limp, for modeling programs that utilize preexisting components. Limp is an extension of the Lustre synchronous data flow language. Limp extends Lustre by introducing control flow elements, global variables, and syntax specifying preconditions, postconditions, and global variable interactions of preexisting components.</p> <p>SIMPAL translates Limp programs to an equivalent Lustre representation which can be passed to the JKind model checking tool to perform assume-guarantee reasoning, reachability, and viability analyses. The feedback from these analyses can be used to refine the program to ensure the software functions as intended.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/etd/16263/
dc.identifier.articleid 7271
dc.identifier.contextkey 11937683
dc.identifier.doi https://doi.org/10.31274/etd-180810-5893
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/16263
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/30446
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/etd/16263/Wagner_iastate_0097M_16274.pdf|||Fri Jan 14 20:57:24 UTC 2022
dc.subject.disciplines Computer Engineering
dc.subject.disciplines Computer Sciences
dc.subject.disciplines Electrical and Electronics
dc.subject.keywords assume-guarantee reasoning
dc.subject.keywords contract-based reasoning
dc.subject.keywords k-induction
dc.subject.keywords model checking
dc.title SIMPAL: A Compositional Reasoning Framework for Imperative Programs
dc.type article
dc.type.genre thesis
dspace.entity.type Publication
relation.isOrgUnitOfPublication a75a044c-d11e-44cd-af4f-dab1d83339ff
thesis.degree.discipline Electrical Engineering
thesis.degree.level thesis
thesis.degree.name Master of Science
File
Original bundle
Now showing 1 - 1 of 1
Name:
Wagner_iastate_0097M_16274.pdf
Size:
593.55 KB
Format:
Adobe Portable Document Format
Description: