Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Brigham Young University

Theses/Dissertations

2005

Model checking

Articles 1 - 2 of 2

Full-Text Articles in Physical Sciences and Mathematics

Dynamic Dead Variable Analysis, Micah S. Lewis Aug 2005

Dynamic Dead Variable Analysis, Micah S. Lewis

Theses and Dissertations

Dynamic dead variable analysis (DDVA) extends traditional static dead variable analysis (SDVA) in the context of model checking through the use of run-time information. The analysis is run multiple times during the course of model checking to create a more precise set of dead variables. The DDVA is evaluated based on the amount of memory used to complete model checking relative to SDVA while considering the extra overhead required to implement DDVA. On several models with a complex control flow graph, DDVA reduces the amount of memory needed by 38-88MB compared to SDVA with a cost of 36 bytes of …


January: Search Based On Social Insect Behavior, Peter C. Lamborn Apr 2005

January: Search Based On Social Insect Behavior, Peter C. Lamborn

Theses and Dissertations

January is a group of interacting stateless model checkers. Each agent functions on a processor located on a super computer or a network of workstations (NOW). The agent's search pattern is a semi-random walk based on the behavior of the grey field slug (Agriolimax reticulatus), the house fly (Musca domestica), and the black ant (Lassius niger). The agents communicate to lessen the amount of duplicate work being done. Every algorithm has a memory threshold above which they search efficiently. This threshold varies not only by model but also by algorithm. Janaury's threshold is lower than the thresholds of other algorithms …