|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
Nondeterministic finite automata (NFA) are widely used in computer science fields, such as regular languages in formal language theory, high-speed network monitoring, image recognition, hardware modeling, or even in bioinformatic for the detection of the sequence of nucleotide acids in DNA. They are also used in regular mode checking, in string solving, in verification of pointer manipulating programs, for construction of linear arithmetic equations and inequalities, for decision in WS1S and WS2S logic, and many others. Automata minimization is a fundamental technique that helps to decrease resource claims (memory, time, or a number of hardware components) of implemented automata and speed up automata operations. Commonly used minimization techniques, such as state merging, transition pruning, and saturation, can leave potentially minimizable automaton subgraphs with duplicit language information. These fragments consist of a group of states, where the part of language of one state is piecewise covered by the other states in this group. The thesis describes a new minimization approach, which uses SAT solver, which provides information for efficient minimization of these so far nonminimizable automaton parts. Moreover, the newly investigated method, which only uses solver information and state merging, can minimize the automaton similarly and on automata with low transition count faster than a tool RABIT/Reduce, which uses state merging and transition pruning.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
Nondeterministic finite automata (NFA) are widely used in computer science fields, such as regular languages in formal language theory, high-speed network monitoring, image recognition, hardware modeling, or even in bioinformatic for the detection of the sequence of nucleotide acids in DNA. They are also used in regular mode checking, in string solving, in verification of pointer manipulating programs, for construction of linear arithmetic equations and inequalities, for decision in WS1S and WS2S logic, and many others. Automata minimization is a fundamental technique that helps to decrease resource claims (memory, time, or a number of hardware components) of implemented automata and speed up automata operations. Commonly used minimization techniques, such as state merging, transition pruning, and saturation, can leave potentially minimizable automaton subgraphs with duplicit language information. These fragments consist of a group of states, where the part of language of one state is piecewise covered by the other states in this group. The thesis describes a new minimization approach, which uses SAT solver, which provides information for efficient minimization of these so far nonminimizable automaton parts. Moreover, the newly investigated method, which only uses solver information and state merging, can minimize the automaton similarly and on automata with low transition count faster than a tool RABIT/Reduce, which uses state merging and transition pruning.
|
host ::
RSS.