Abstraction Based Techniques for Constrained Horn Clause Solving. Somorjai, M. 2022. Bachelor's Thesis, Budapest University of Technology and Economics![Abstraction Based Techniques for Constrained Horn Clause Solving [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Pdf ![Abstraction Based Techniques for Constrained Horn Clause Solving [link]](https://bibbase.org/img/filetypes/link.svg "link")
Link abstract bibtex 5 downloads Software components of safety-critical systems are becoming more and more complex. Failure in a safety-critical system can lead to enormous financial loss, environmental dam- age, or even loss of life; thereby, the correctness of such systems needs to be ensured. Conventional testing can not be exhaustive in reasonable time, leaving the need to prove the safety of programs in other ways. Formal verification takes on this task by provid- ing a mathematically precise proof of correctness or refutation to the safety properties of programs, such as the reachability of an erroneous state. Formal verification works on formal models of programs, one such formalism being the Control Flow Automaton (CFA). It is a graph-like notation to represent programs, in which erroneous locations map to specific nodes that should be unreachable. Another formalism that is widely used as an intermediate language in the verification process is Constrained Horn Clauses (CHCs). They can describe programs and their desired properties in a well-defined subset of first-order logic formulae on variables and uninterpreted functions. Therefore the question of correctness in this representation is embodied in the satisfiability of a query, which can be decided by SMT solvers designed to determine the satisfiability of mathematical formulae. Conventionally, one approach to deciding reachability in CFAs has been to transform the model into CHCs and utilize an SMT solver to find a satisfying model. However, this task tends to be difficult for SMT solvers due to the exponential number of possible assignments with respect to the number of variables and predicates. In contrast, in this work, I propose an approach to solving CHCs by transforming them into a CFA, which provides access to powerful abstraction-refinement-based model checking algorithms. Such algorithms employ abstraction to reduce the space of possible assignments, which could potentially lead to significant improvements in efficiency compared to traditional CHC solving techniques. I evaluate my approach both on synthetic and industrial examples.
@misc{somorjaimBsc2022,
author = {Somorjai, M\'ark},
title = {Abstraction Based Techniques for Constrained Horn Clause Solving},
note = {Bachelor's Thesis, Budapest University of Technology and Economics},
year = {2022},
type = {Thesis},
url_pdf = {somorjaimBsc2022.pdf},
url_link = {https://diplomaterv.vik.bme.hu/hu/Theses/Absztrakcio-alapu-technikak-CHC-problemak},
abstract = {Software components of safety-critical systems are becoming more and more complex. Failure in a safety-critical system can lead to enormous financial loss, environmental dam- age, or even loss of life; thereby, the correctness of such systems needs to be ensured. Conventional testing can not be exhaustive in reasonable time, leaving the need to prove the safety of programs in other ways. Formal verification takes on this task by provid- ing a mathematically precise proof of correctness or refutation to the safety properties of programs, such as the reachability of an erroneous state. Formal verification works on formal models of programs, one such formalism being the Control Flow Automaton (CFA). It is a graph-like notation to represent programs, in which erroneous locations map to specific nodes that should be unreachable. Another formalism that is widely used as an intermediate language in the verification process is Constrained Horn Clauses (CHCs). They can describe programs and their desired properties in a well-defined subset of first-order logic formulae on variables and uninterpreted functions. Therefore the question of correctness in this representation is embodied in the satisfiability of a query, which can be decided by SMT solvers designed to determine the satisfiability of mathematical formulae. Conventionally, one approach to deciding reachability in CFAs has been to transform the model into CHCs and utilize an SMT solver to find a satisfying model. However, this task tends to be difficult for SMT solvers due to the exponential number of possible assignments with respect to the number of variables and predicates. In contrast, in this work, I propose an approach to solving CHCs by transforming them into a CFA, which provides access to powerful abstraction-refinement-based model checking algorithms. Such algorithms employ abstraction to reduce the space of possible assignments, which could potentially lead to significant improvements in efficiency compared to traditional CHC solving techniques. I evaluate my approach both on synthetic and industrial examples.},
}
Downloads: 5
{"_id":"rBCC4TcDbp46kCufn","bibbaseid":"somorjai-abstractionbasedtechniquesforconstrainedhornclausesolving-2022","author_short":["Somorjai, M."],"bibdata":{"bibtype":"misc","type":"Thesis","author":[{"propositions":[],"lastnames":["Somorjai"],"firstnames":["Márk"],"suffixes":[]}],"title":"Abstraction Based Techniques for Constrained Horn Clause Solving","note":"Bachelor's Thesis, Budapest University of Technology and Economics","year":"2022","url_pdf":"somorjaimBsc2022.pdf","url_link":"https://diplomaterv.vik.bme.hu/hu/Theses/Absztrakcio-alapu-technikak-CHC-problemak","abstract":"Software components of safety-critical systems are becoming more and more complex. Failure in a safety-critical system can lead to enormous financial loss, environmental dam- age, or even loss of life; thereby, the correctness of such systems needs to be ensured. Conventional testing can not be exhaustive in reasonable time, leaving the need to prove the safety of programs in other ways. Formal verification takes on this task by provid- ing a mathematically precise proof of correctness or refutation to the safety properties of programs, such as the reachability of an erroneous state. Formal verification works on formal models of programs, one such formalism being the Control Flow Automaton (CFA). It is a graph-like notation to represent programs, in which erroneous locations map to specific nodes that should be unreachable. Another formalism that is widely used as an intermediate language in the verification process is Constrained Horn Clauses (CHCs). They can describe programs and their desired properties in a well-defined subset of first-order logic formulae on variables and uninterpreted functions. Therefore the question of correctness in this representation is embodied in the satisfiability of a query, which can be decided by SMT solvers designed to determine the satisfiability of mathematical formulae. Conventionally, one approach to deciding reachability in CFAs has been to transform the model into CHCs and utilize an SMT solver to find a satisfying model. However, this task tends to be difficult for SMT solvers due to the exponential number of possible assignments with respect to the number of variables and predicates. In contrast, in this work, I propose an approach to solving CHCs by transforming them into a CFA, which provides access to powerful abstraction-refinement-based model checking algorithms. Such algorithms employ abstraction to reduce the space of possible assignments, which could potentially lead to significant improvements in efficiency compared to traditional CHC solving techniques. I evaluate my approach both on synthetic and industrial examples.","bibtex":"@misc{somorjaimBsc2022,\n author = {Somorjai, M\\'ark},\n title = {Abstraction Based Techniques for Constrained Horn Clause Solving},\n note = {Bachelor's Thesis, Budapest University of Technology and Economics},\n year = {2022},\n type = {Thesis},\n url_pdf = {somorjaimBsc2022.pdf},\n url_link = {https://diplomaterv.vik.bme.hu/hu/Theses/Absztrakcio-alapu-technikak-CHC-problemak},\n abstract = {Software components of safety-critical systems are becoming more and more complex. Failure in a safety-critical system can lead to enormous financial loss, environmental dam- age, or even loss of life; thereby, the correctness of such systems needs to be ensured. Conventional testing can not be exhaustive in reasonable time, leaving the need to prove the safety of programs in other ways. Formal verification takes on this task by provid- ing a mathematically precise proof of correctness or refutation to the safety properties of programs, such as the reachability of an erroneous state. Formal verification works on formal models of programs, one such formalism being the Control Flow Automaton (CFA). It is a graph-like notation to represent programs, in which erroneous locations map to specific nodes that should be unreachable. Another formalism that is widely used as an intermediate language in the verification process is Constrained Horn Clauses (CHCs). They can describe programs and their desired properties in a well-defined subset of first-order logic formulae on variables and uninterpreted functions. Therefore the question of correctness in this representation is embodied in the satisfiability of a query, which can be decided by SMT solvers designed to determine the satisfiability of mathematical formulae. Conventionally, one approach to deciding reachability in CFAs has been to transform the model into CHCs and utilize an SMT solver to find a satisfying model. However, this task tends to be difficult for SMT solvers due to the exponential number of possible assignments with respect to the number of variables and predicates. In contrast, in this work, I propose an approach to solving CHCs by transforming them into a CFA, which provides access to powerful abstraction-refinement-based model checking algorithms. Such algorithms employ abstraction to reduce the space of possible assignments, which could potentially lead to significant improvements in efficiency compared to traditional CHC solving techniques. I evaluate my approach both on synthetic and industrial examples.},\n}\n\n","author_short":["Somorjai, M."],"key":"somorjaimBsc2022","id":"somorjaimBsc2022","bibbaseid":"somorjai-abstractionbasedtechniquesforconstrainedhornclausesolving-2022","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/somorjaimBsc2022.pdf"," link":"https://diplomaterv.vik.bme.hu/hu/Theses/Absztrakcio-alapu-technikak-CHC-problemak"},"metadata":{"authorlinks":{}},"downloads":5},"bibtype":"misc","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","dataSources":["7MDizr2BZojXoNdPN"],"keywords":[],"search_terms":["abstraction","based","techniques","constrained","horn","clause","solving","somorjai"],"title":"Abstraction Based Techniques for Constrained Horn Clause Solving","year":2022,"downloads":5}