| 
|
QuoteRef: chouA11_2000
topics >
all references >
ThesaHelp:
ACM references a-e
ThesaHelp:
references c-d
Topic:
compiler error checking
Topic:
debugging by usage rules
Topic:
path expression
Topic:
communication protocols
Topic:
state machine
Topic:
pattern matching
Topic:
extensible languages
Topic:
model checker
Topic:
program proving is infeasible
Reference
Chou, A., Chelf, B., Engler, D., Heinrich, M., "Using meta-level compilation to check FLASH protocol code", Proceedings of the ninth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS IX), ACM SIGPLAN, 35, 11, November 2000, Cambridge MA, pp. 59-70. Google
59 ;;Quote: use meta-level compilation (MC) to easily check path invariants; simple description, complicated source of errors, maintained across all paths; e.g., for cache coherence
59+;;Quote: meta-level compiler extensions pinpoints errors with 10-100 lines written in a few days; avoids complex errors
59 ;;Quote: check system invariants through compiler extensions; found 34 bugs in a well-tested, cache coherence protocol; short, easily written
61 ;;Quote: meta-level compilation through extensible compiler with high-level state machines applied down every path; transitions triggered by patterns
61 ;;Quote: check restrictions of the following types; Never/Always do X, Always do X before/after Y, If you do X then you must/cannot do Y
68 ;;Quote: model checkers find a few difficult errors with simplified code; meta-level compilation works directly with program source and found many errors
ThesaHelp: ACM references a-e (259 items)
ThesaHelp: references c-d (337 items)
Topic: compiler error checking (16 items)
Topic: debugging by usage rules (40 items)
Topic: path expression (14 items)
Topic: communication protocols (61 items)
Topic: state machine (67 items)
Topic: pattern matching (42 items)
Topic: extensible languages (69 items)
Topic: model checker (49 items)
Topic: program proving is infeasible (46 items)