Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 12 of 12 for “"Abstraction Refinement"”.
-
Analysis of dynamic evolution systems by spotlight abstraction refinement
Diese Arbeit entwickelt eine formale Analysemethode für Systemmodelle mit einer sich verändernden Prozessanzahl und Verbindungsstruktur. Wir benutzen die Technik der Spotlight-Abstraktion um eine endliche Darstellung des Gesamtsystems und der zu prüfenden Eigenschaft zu erhalten. Basierend auf dem …
-
Effective Approaches to Abstraction Refinement for Automatic Software Verification
… From this insight we infer that some form of abstraction technique must be added to the value analysis in order to also allow the successful verification of large and complex verification tasks. As a solution, we propose to incorporate counterexample-guided abstraction refinement (CEGAR) and …
-
An algebraic model of software evolution
… of the software evolution process, called the Abstraction Refinement Model, is described which builds on the algebraic influence of the Laws of Programming and the transformational Draco Paradigm. The result is an algebraic structure consisting of the states of the software product (system …
-
Program Synthesis over Noisy Data
… noisy program synthesis algorithm that uses an abstraction refinement based optimization process to synthesize programs. The presented experimental results demonstrate the significant performance improvements that this new technique can deliver. Building on this abstraction refinement technique, …
-
Exploring Abstraction Techniques for Scalable Bit-Precise Verification of Embedded Software
… intractably large. In this dissertation, several abstraction techniques are explored to deal with this scalability challenge in the bit-precise verification of embedded software. First, we propose a tight integration of program slicing, which is an important static program analysis technique, with …
-
Remedies for building reliable cyber-physical systems
… in this thesis is a counter-example guided abstraction refinement algorithm for unbounded time model checking of non- linear hybrid automata. Clearly, this is an undecidable problem and that is the main reason for using abstraction refinement techniques. Our CEGAR framework for this class is …
-
Design Verification for Sequential Systems at Various Abstraction Levels
… utilizes different core algorithms at various abstraction levels. At the logic level, we focus on incorporating a set of novel ideas to existing formal verification approaches. First, we present a number of powerful optimizations to improve the performance and capacity of a typical SAT-based …
-
Formal verification-driven parallelisation synthesis
… specifications, and counterexample-guided abstraction refinement to confirm or refute the equivalence between the conjectured specification and the original program. Once equivalence checking succeeds, from the inferred specifications we synthesise code that executes speculatively in …
-
Methodology of refinement and decomposition in UML-B
… supported in plain Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same abstraction-refinement concepts can also be applied in UML-B. This work introduces the notions of refined classes, refined state machines and extended classtypes to …
-
SMT-based bounded model checking of multi-threaded software in embedded systems
… context-bounding or counterexample-guided abstraction refinement.
-
Approximation Based Safety and Stability Verification of Hybrid Systems
… we propose a novel ""counterexample guided abstraction refinement"" (CEGAR) technique called ""hybrid CEGAR"", which constructs a hybrid abstraction of a system unlike the previous methods which were based on constructing finite state abstractions. Our method has several advantages in terms …
-
Search State Extensibility based Learning Framework for Model Checking and Test Generation
… computation is later leveraged to create an abstraction-refinement based model checking framework. During Manufacturing Test, test patterns are applied to the fabricated system, in a test environment, to check for the existence of fabrication defects. Such patterns are usually generated by …