Paper Info
Title
A MuDDy Experience---ML Bindings to a BDD Library
Abstract
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).
Year
DOI
Venue
2009
10.1007/978-3-642-03034-5_3
DSL
Keywords
Field
DocType
high-performance c library,c library,bdd package buddy,ml bindings,core data structure,domain specific embedded language,ml interface,standard ml,muddy experience,data structure,binary decision diagrams,domain specific language,bdd library,finite state machine,binary decision diagram,canonical form,model checking
Domain-specific language,Data structure,Programming language,Standard ML,Computer science,Binary decision diagram,Canonical form,Theoretical computer science,Symbolic execution,Boolean expression,Caml
Conference
Volume
ISSN
Citations 
5658
0302-9743
0
PageRank 
References 
Authors
0.34
9
1
Name
Order
Citations
PageRank
Ken Friis Larsen1535.14