Back to Search
Start Over
Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata
- Source :
- Lecture Notes in Computer Science ISBN: 9783030634605, IFM
- Publication Year :
- 2020
- Publisher :
- Springer International Publishing, 2020.
-
Abstract
- We develop a complementation procedure and an equivalence checker for nondeterministic Buchi automata. Both are formally verified using the proof assistant Isabelle/Hol. The verification covers everything from the abstract correctness proof down to the generated Sml code.
- Subjects :
- 050101 languages & linguistics
Programming language
Computer science
05 social sciences
Proof assistant
Formal equivalence checking
Büchi automaton
HOL
02 engineering and technology
computer.file_format
computer.software_genre
Nondeterministic algorithm
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
0501 psychology and cognitive sciences
Executable
Software_PROGRAMMINGLANGUAGES
computer
Equivalence (measure theory)
Formal verification
Subjects
Details
- ISBN :
- 978-3-030-63460-5
- ISBNs :
- 9783030634605
- Database :
- OpenAIRE
- Journal :
- Lecture Notes in Computer Science ISBN: 9783030634605, IFM
- Accession number :
- edsair.doi...........4fbc9d0a6a81feca5ef300d64faa67a9
- Full Text :
- https://doi.org/10.1007/978-3-030-63461-2_13