Monadic second-order logic: Difference between revisions

Revision as of 04:20, 3 January 2021

Revision as of 15:21, 28 July 2021

Line 38:

=== Use of satisfiability of MSO on trees in verification ===

Monadic second-order logic of trees has applications in [[Software verification]] and, more broadly, [[Formal verification]] thanks to its decidability and significant expressive power. Decision procedures for satisfiability have been implemented.<ref>{{Cite journal|last=Henriksen|first=Jesper G.|last2=Jensen|first2=Jakob|last3=Jørgensen|first3=Michael|last4=Klarlund|first4=Nils|last5=Paige|first5=Robert|last6=Rauhe|first6=Theis|last7=Sandholm|first7=Anders|date=1995|editor-last=Brinksma|editor-first=E.|editor2-last=Cleaveland|editor2-first=W. R.|editor3-last=Larsen|editor3-first=K. G.|editor4-last=Margaria|editor4-first=T.|editor5-last=Steffen|editor5-first=B.|title=Mona: Monadic second-order logic in practice|url=https://link.springer.com/chapter/10.1007/3-540-60630-0_5|journal=Tools and Algorithms for the Construction and Analysis of Systems|series=Lecture Notes in Computer Science|language=en|___location=Berlin, Heidelberg|publisher=Springer|pages=89–110|doi=10.1007/3-540-60630-0_5|isbn=978-3-540-48509-4|doi-access=free}}</ref><ref>{{Cite journal|last=Fiedor|first=Tomáš|last2=Holík|first2=Lukáš|last3=Lengál|first3=Ondřej|last4=Vojnar|first4=Tomáš|date=2019-04-01|title=Nested antichains for WS1S|url=https://doi.org/10.1007/s00236-018-0331-z|journal=Acta Informatica|language=en|volume=56|issue=3|pages=205–228|doi=10.1007/s00236-018-0331-z|issn=1432-0525}}</ref><ref>{{Cite journal|last=Traytel|first=Dmitriy|last2=Nipkow|first2=Tobias|date=2013-09-25|title=Verified decision procedures for MSO on words based on derivatives of regular expressions|url=https://doi.org/10.1145/2544174.2500612|journal=ACM SIGPLAN Notices|volume=48|issue=9|pages=3–123–f12|doi=10.1145/2544174.2500612|issn=0362-1340|hdl=20.500.11850/106053|hdl-access=free}}</ref> Such procedures were used to prove properties of programs manipulating linked data structures,<ref>{{Cite journal|last=Møller|first=Anders|last2=Schwartzbach|first2=Michael I.|date=2001-05-01|title=The pointer assertion logic engine|url=https://doi.org/10.1145/378795.378851|journal=Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation|series=PLDI '01|___location=Snowbird, Utah, USA|publisher=Association for Computing Machinery|pages=221–231|doi=10.1145/378795.378851|isbn=978-1-58113-414-8}}</ref> as a form of [[Shape analysis (program analysis)|Shape analysis]] as well as for symbolic reasoning in hardware verification.<ref>{{Cite journal|last=Basin|first=David|last2=Klarlund|first2=Nils|date=1998-11-01|title=Automata based symbolic reasoning in hardware verification|url=https://doi.org/10.1023/A:1008644009416|journal=Formal Methods in System Design|volume=13|issue=3|pages=255–288|doi=10.1023/A:1008644009416|issn=0925-9856}}</ref>

==References==