A MuDDy Experience-ML Bindings to a BDD Library
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
A MuDDy Experience-ML Bindings to a BDD Library. / Larsen, Ken Friis.
Domain-Specific Languages, IFIP TC 2 Working Conference, DSL 2009. ed. / Walid Mohamed Taha. Vol. 5658 Springer, 2009. p. 45-57 (Lecture notes in computer science, Vol. 5658).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - A MuDDy Experience-ML Bindings to a BDD Library
AU - Larsen, Ken Friis
PY - 2009
Y1 - 2009
N2 - Binary Decision Diagrams (BDDs) are a data structure used to efficiently represent boolean expressions on canonical form. BDDs are often the core data structure in model checkers. MuDDy is an ML interface (both for Standard ML and Objective Caml) to the BDD package BuDDy that is written in C. This combination of an ML interface to a high-performance C library is surprisingly fruitful. ML allows you to quickly experiment with high-level symbolic algorithms before handing over the grunt work to the C library. I show how, with a relatively little effort, you can make a domain specific language for concurrent finite state-machines embedded in Standard ML and then write various custom model-checking algorithms for this domain specific embedded language (DSEL).
AB - Binary Decision Diagrams (BDDs) are a data structure used to efficiently represent boolean expressions on canonical form. BDDs are often the core data structure in model checkers. MuDDy is an ML interface (both for Standard ML and Objective Caml) to the BDD package BuDDy that is written in C. This combination of an ML interface to a high-performance C library is surprisingly fruitful. ML allows you to quickly experiment with high-level symbolic algorithms before handing over the grunt work to the C library. I show how, with a relatively little effort, you can make a domain specific language for concurrent finite state-machines embedded in Standard ML and then write various custom model-checking algorithms for this domain specific embedded language (DSEL).
U2 - 10.1007/978-3-642-03034-5_3
DO - 10.1007/978-3-642-03034-5_3
M3 - Article in proceedings
SN - 978-3-642-03033-8
VL - 5658
T3 - Lecture notes in computer science
SP - 45
EP - 57
BT - Domain-Specific Languages, IFIP TC 2 Working Conference, DSL 2009
A2 - Taha, Walid Mohamed
PB - Springer
Y2 - 15 July 2009 through 17 July 2009
ER -
ID: 19345434