{"id":{"repo_id":"freiburg-diss","oai_identifier":"oai:freidok.uni-freiburg.de:791"},"canonical_url":"https://search.dev.ndltd.org/etd/freiburg-diss/oai:freidok.uni-freiburg.de:791","repository":{"repo_id":"freiburg-diss","name":"University of Freiburg","base_url":"https://freidok.uni-freiburg.de/oai/oai2.php"},"display":{"title":"Directed search for the verification of communication protocols","abstract":"There is a need for formal methods to verify correctness of software
and hardware systems. Automated verification techniques basically
explore the state space of a system in order to establish whether or
not it behaves correctly. The main drawback of such methods is the state explosion problem. The size of the state space can grow
exponentially in the number of components of the system, especially in
asynchronous concurrent systems. In early stages of system
development, errors are likely to appear. As a matter of fact, in practice,
automated verification has been shown to be more successful in finding errors in
systems than in proving correctness. Usually, one applies reachability algorithms like
depth-first, and breadth-first search for this purpose. Breadth-first
search is, in general, not memory-efficient, but offers shortest
counterexamples. On the other hand, depth-first search is more
memory-efficient, but delivers suboptimal counterexamples.
We propose and analyze the use of classic heuristic search
algorithms for a more efficient error detection. First, heuristic
search can help mitigate the effects of the state explosion
problem by guidining the search into error states. Second, some of these
algorithms can guarantee optimal counterexamples. This is important
for the error correction process since, in general, the shorter a
counterexample is, the easier it is to understand what it really means.
We distinguish two main problems: finding an error quickly, and
finding a short(est) counterexample. Each problem has different
requirements and calls for different strategies.
Heuristic functions are applied to guide the search. We propose
and analyze several such functions. Moreover, we analyze how heuristic
search combines with other techniques usually applied to avoid the
state explosion problem, namely partial order reduction and bitstate hashing.
We basically concentrate on the detection of
safety errors, which are just reach","abstract_html":"There is a need for formal methods to verify correctness of software <br>and hardware systems. Automated verification techniques basically <br>explore the state space of a system in order to establish whether or <br>not it behaves correctly. The main drawback of such methods is the state explosion problem. The size of the state space can grow <br>exponentially in the number of components of the system, especially in <br>asynchronous concurrent systems. In early stages of system <br>development, errors are likely to appear. As a matter of fact, in practice, <br>automated verification has been shown to be more successful in finding errors in <br>systems than in proving correctness. Usually, one applies reachability algorithms like <br>depth-first, and breadth-first search for this purpose. Breadth-first <br>search is, in general, not memory-efficient, but offers shortest <br>counterexamples. On the other hand, depth-first search is more <br>memory-efficient, but delivers suboptimal counterexamples. <br> <br>We propose and analyze the use of classic heuristic search <br>algorithms for a more efficient error detection. First, heuristic <br>search can help mitigate the effects of the state explosion <br>problem by guidining the search into error states. Second, some of these <br>algorithms can guarantee optimal counterexamples. This is important <br>for the error correction process since, in general, the shorter a <br>counterexample is, the easier it is to understand what it really means. <br> <br>We distinguish two main problems: finding an error quickly, and <br>finding a short(est) counterexample. Each problem has different <br>requirements and calls for different strategies. <br>Heuristic functions are applied to guide the search. We propose <br>and analyze several such functions. Moreover, we analyze how heuristic <br>search combines with other techniques usually applied to avoid the <br>state explosion problem, namely partial order reduction and bitstate hashing. <br> <br>We basically concentrate on the detection of <br>safety errors, which are just reach","abstract_has_math":false,"creators":["Lluch Lafuente, Alberto"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Ottmann, Thomas"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T02:21:58Z","subjects":[],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://freidok.uni-freiburg.de/data/791","outbound_label":"Repository record","outbound_source":"source_url"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Ottmann, Thomas"]},{"key":"dc:creator","label":"Author","values":["Lluch Lafuente, Alberto"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:type","label":"Dc Type","values":["DoctoralThesis"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["There is a need for formal methods to verify correctness of software
and hardware systems. Automated verification techniques basically
explore the state space of a system in order to establish whether or
not it behaves correctly. The main drawback of such methods is the state explosion problem. The size of the state space can grow
exponentially in the number of components of the system, especially in
asynchronous concurrent systems. In early stages of system
development, errors are likely to appear. As a matter of fact, in practice,
automated verification has been shown to be more successful in finding errors in
systems than in proving correctness. Usually, one applies reachability algorithms like
depth-first, and breadth-first search for this purpose. Breadth-first
search is, in general, not memory-efficient, but offers shortest
counterexamples. On the other hand, depth-first search is more
memory-efficient, but delivers suboptimal counterexamples.
We propose and analyze the use of classic heuristic search
algorithms for a more efficient error detection. First, heuristic
search can help mitigate the effects of the state explosion
problem by guidining the search into error states. Second, some of these
algorithms can guarantee optimal counterexamples. This is important
for the error correction process since, in general, the shorter a
counterexample is, the easier it is to understand what it really means.
We distinguish two main problems: finding an error quickly, and
finding a short(est) counterexample. Each problem has different
requirements and calls for different strategies.
Heuristic functions are applied to guide the search. We propose
and analyze several such functions. Moreover, we analyze how heuristic
search combines with other techniques usually applied to avoid the
state explosion problem, namely partial order reduction and bitstate hashing.
We basically concentrate on the detection of
safety errors, which are just reach"]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["application/pdf","application/x-zip-compressed"]},{"key":"dc:title","label":"Title","values":["Directed search for the verification of communication protocols","Gerichtete Suche für die Verifikation von Kommunikationsprotokollen"]}]}],"canonical_facts":{"dc:contributor":["Ottmann, Thomas"],"dc:creator":["Lluch Lafuente, Alberto"],"dc:description.abstract":["There is a need for formal methods to verify correctness of software
and hardware systems. Automated verification techniques basically
explore the state space of a system in order to establish whether or
not it behaves correctly. The main drawback of such methods is the state explosion problem. The size of the state space can grow
exponentially in the number of components of the system, especially in
asynchronous concurrent systems. In early stages of system
development, errors are likely to appear. As a matter of fact, in practice,
automated verification has been shown to be more successful in finding errors in
systems than in proving correctness. Usually, one applies reachability algorithms like
depth-first, and breadth-first search for this purpose. Breadth-first
search is, in general, not memory-efficient, but offers shortest
counterexamples. On the other hand, depth-first search is more
memory-efficient, but delivers suboptimal counterexamples.
We propose and analyze the use of classic heuristic search
algorithms for a more efficient error detection. First, heuristic
search can help mitigate the effects of the state explosion
problem by guidining the search into error states. Second, some of these
algorithms can guarantee optimal counterexamples. This is important
for the error correction process since, in general, the shorter a
counterexample is, the easier it is to understand what it really means.
We distinguish two main problems: finding an error quickly, and
finding a short(est) counterexample. Each problem has different
requirements and calls for different strategies.
Heuristic functions are applied to guide the search. We propose
and analyze several such functions. Moreover, we analyze how heuristic
search combines with other techniques usually applied to avoid the
state explosion problem, namely partial order reduction and bitstate hashing.
We basically concentrate on the detection of
safety errors, which are just reach"],"dc:format.medium":["application/pdf","application/x-zip-compressed"],"dc:title":["Directed search for the verification of communication protocols","Gerichtete Suche für die Verifikation von Kommunikationsprotokollen"],"dc:type":["DoctoralThesis"]},"updated_at":"2026-07-24T02:21:58Z"}