{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:59420"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:59420","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Verification of Erlang programs using abstract interpretation and model checking","abstract":"The functional programming language Erlang is successfully used for the development of distributed systems. We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. Therefore, we define a framework for abstract interpretations of Erlang programs. In this framework it is guaranteed that the abstract operational semantics is safe with respect to the standard semantics of Erlang. In this context, safe means that it contains all paths of the standard semantics. Applying this framework to a finite domain abstraction, many system properties (e.g. the absence of deadlocks and lifelocks or mutual exclusion) can automatically be proven by model checking. Since the framework guarantees safeness of the abstraction the properties proven for the abstraction also hold for the real execution of the Erlang program. In this theses, we develop the framework for abstract interpretations of Erlang programs for formal verification by model checking. We show how the framework can be used in model checking for Linear Time Logic. For Erlang programs containing non-tail recursive function calls data abstraction covered by our framework is not sufficient. Therefore, we extend the framework by abstraction of the control-flow. All presented techniques are prototypically implemented in a verification tool. We demonstrate the practical usability of our approach and the verification tool by the verification of a database server.","abstract_html":"The functional programming language Erlang is successfully used for the development of distributed systems. We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. Therefore, we define a framework for abstract interpretations of Erlang programs. In this framework it is guaranteed that the abstract operational semantics is safe with respect to the standard semantics of Erlang. In this context, safe means that it contains all paths of the standard semantics. Applying this framework to a finite domain abstraction, many system properties (e.g. the absence of deadlocks and lifelocks or mutual exclusion) can automatically be proven by model checking. Since the framework guarantees safeness of the abstraction the properties proven for the abstraction also hold for the real execution of the Erlang program. In this theses, we develop the framework for abstract interpretations of Erlang programs for formal verification by model checking. We show how the framework can be used in model checking for Linear Time Logic. For Erlang programs containing non-tail recursive function calls data abstraction covered by our framework is not sufficient. Therefore, we extend the framework by abstraction of the control-flow. All presented techniques are prototypically implemented in a verification tool. We demonstrate the practical usability of our approach and the verification tool by the verification of a database server.","abstract_has_math":false,"creators":["Huch, Frank Günter"],"institution":"Publikationsserver der RWTH Aachen University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Indermark, Klaus"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2001,"date_issued":"2001","date_published":"2001","updated_at":"2026-07-30T19:42:39Z","subjects":["info:eu-repo/classification/ddc/004","Informatik","Verteiltes System","Softwareentwicklung","Funktionale Programmiersprache","Programmverifikation","Model checking","Abstrakte Interpretation","Erlang","Verification","Abstraction"],"languages":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-121207%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-121207%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-121207%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/59420","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Indermark, Klaus"]},{"key":"dc:creator","label":"Author","values":["Huch, Frank Günter"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2001"]},{"key":"dc:publisher","label":"Institution","values":["Publikationsserver der RWTH Aachen University"]},{"key":"dc:relation","label":"Dc Relation","values":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-4303"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["info:eu-repo/classification/ddc/004","Informatik","Verteiltes System","Softwareentwicklung","Funktionale Programmiersprache","Programmverifikation","Model checking","Abstrakte Interpretation","Erlang","Verification","Abstraction"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/record/59420","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-121207%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The functional programming language Erlang is successfully used for the development of distributed systems. We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. Therefore, we define a framework for abstract interpretations of Erlang programs. In this framework it is guaranteed that the abstract operational semantics is safe with respect to the standard semantics of Erlang. In this context, safe means that it contains all paths of the standard semantics. Applying this framework to a finite domain abstraction, many system properties (e.g. the absence of deadlocks and lifelocks or mutual exclusion) can automatically be proven by model checking. Since the framework guarantees safeness of the abstraction the properties proven for the abstraction also hold for the real execution of the Erlang program. In this theses, we develop the framework for abstract interpretations of Erlang programs for formal verification by model checking. We show how the framework can be used in model checking for Linear Time Logic. For Erlang programs containing non-tail recursive function calls data abstraction covered by our framework is not sufficient. Therefore, we extend the framework by abstraction of the control-flow. All presented techniques are prototypically implemented in a verification tool. We demonstrate the practical usability of our approach and the verification tool by the verification of a database server."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University X, 148 S. (2001). = Aachen, Techn. Hochsch., Diss., 2001"]},{"key":"dc:title","label":"Title","values":["Verification of Erlang programs using abstract interpretation and model checking"]}]}],"canonical_facts":{"dc:contributor":["Indermark, Klaus"],"dc:coverage":["DE"],"dc:creator":["Huch, Frank Günter"],"dc:date":["2001"],"dc:description":["The functional programming language Erlang is successfully used for the development of distributed systems. We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. Therefore, we define a framework for abstract interpretations of Erlang programs. In this framework it is guaranteed that the abstract operational semantics is safe with respect to the standard semantics of Erlang. In this context, safe means that it contains all paths of the standard semantics. Applying this framework to a finite domain abstraction, many system properties (e.g. the absence of deadlocks and lifelocks or mutual exclusion) can automatically be proven by model checking. Since the framework guarantees safeness of the abstraction the properties proven for the abstraction also hold for the real execution of the Erlang program. In this theses, we develop the framework for abstract interpretations of Erlang programs for formal verification by model checking. We show how the framework can be used in model checking for Linear Time Logic. For Erlang programs containing non-tail recursive function calls data abstraction covered by our framework is not sufficient. Therefore, we extend the framework by abstraction of the control-flow. All presented techniques are prototypically implemented in a verification tool. We demonstrate the practical usability of our approach and the verification tool by the verification of a database server."],"dc:identifier":["https://publications.rwth-aachen.de/record/59420","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-121207%22"],"dc:language":["eng"],"dc:publisher":["Publikationsserver der RWTH Aachen University"],"dc:relation":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-4303"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University X, 148 S. (2001). = Aachen, Techn. Hochsch., Diss., 2001"],"dc:subject":["info:eu-repo/classification/ddc/004","Informatik","Verteiltes System","Softwareentwicklung","Funktionale Programmiersprache","Programmverifikation","Model checking","Abstrakte Interpretation","Erlang","Verification","Abstraction"],"dc:title":["Verification of Erlang programs using abstract interpretation and model checking"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:42:39Z"}