Digitale Hardware/ Software-Systeme- P20

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:30

Thêm vào BST

Báo xấu

66
lượt xem 5
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Digitale Hardware/ Software-Systeme- P20:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software- System heutzutage der Stand der Technik. Die Minimierung von Fehlern im Entwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation, also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gesteckt als in den eigentlichen Entwurf....

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Digitale Hardware/ Software-Systeme- P20

564 Literatur 52. B JESSE , P. und K. C LAESSEN: SAT-Based Veriﬁcation without State Space Traversal. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), Seiten 372–389, 2000. ´ 53. B OUL E , M. und Z. Z ILIC: Efﬁcient Automata-Based Assertion-Checker Synthesis of PSL Properties. In: Proceedings of the High-Level Design Validation and Test Workshop (HLDVT), Seiten 69–76, 2006. ´ 54. B OUL E , M. und Z. Z ILIC: Efﬁcient Automata-Based Assertion-Checker Synthesis of SEREs for Hardware Emulation. In: Proceedings of the Asia and South Paciﬁc Design Automation Conference (ASPDAC), Seiten 324–329, 2007. ´ 55. B OUL E , M. und Z. Z ILIC: Automata-Based Assertion-Checker Synthesis of PSL Pro- perties. ACM Transactions on Design Automation of Electronic Systems (TODAES), 13(1):1–21, 2008. 56. B OZZANO , M., R. B RUTTOMESSO, A. C IMATTI, T. J UNTTILA, P. VAN ROSSUM, S. S CHULZ und R. S EBASTIANI: An Incremental and Layered Procedure for the Sa- tisﬁability of Linear Arithmetic Logic. In: Tools and Algorithms for the Construction and Analysis of Systems, Seiten 317–333. Springer, Berlin, Heidelberg, 2005. 57. B RACE , K. S., R. L. RUDELL und R. E. B RYANT: Efﬁcient Implementation of a BDD Package. In: Proceedings of the Design Automation Conference (DAC), Seiten 40–45, 1990. 58. B RAND , D.: Veriﬁcation of Large Synthesized Designs. In: Proceedings of the Interna- tional Conference on Computer-Aided Design (ICCAD), Seiten 534–537, 1993. 59. B RINKMANN , R. und R. D RECHSLER: RTL-Datapath Veriﬁcation using Integer Line- ar Programming. In: Proceedings of the Asia and South Paciﬁc Design Automation Conference (ASPDAC), Seiten 741–746, 2002. 60. B RYANT, R., D. K ROENING, J. O UAKNINE, S. A. S ESHIA, O. S TRICHMAN und B. B RADY: Deciding Bit-Vector Arithmetic with Abstraction. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Seiten 358–372, 2007. 61. B RYANT, R. E.: Symbolic Veriﬁcation of MOS Circuits. In: Chapel Hill Conference on VLSI, Seiten 419–438, 1985. 62. B RYANT, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986. 63. B RYANT, R. E.: On the Complexity of VLSI Implementations and Graph Representati- ons of Boolean Functions with Application to Integer Multiplication. IEEE Transactions on Computers, 40(2):205–213, 1991. 64. B RYANT, R. E., D. B EATTY, K. B RACE, K. C HO und T. S HEFFLER: COSMOS: A Compiled Simulator for MOS Circuits. In: Proceedings of the Design Automation Con- ference (DAC), Seiten 9–16, 1987. 65. B RYANT, R. E. und Y.-A. C HEN: Veriﬁcation of Arithmetic Functions with Binary Mo- ment Diagrams. Technischer Bericht CS-94-160, Carnegie Mellon University, 1994. 66. B RYANT, R. E. und Y.-A. C HEN: Veriﬁcation of Arithmetic Circuits with Binary Mo- ment Diagrams. In: Proceedings of the Design Automation Conference (DAC), Seiten 535–541, 1995. 67. B RYANT, R. E., S. G ERMAN und M. N. V ELEV: Processor Veriﬁcation Using Efﬁ- cient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. ACM Transactions on Computational Logic (TOCL), 2(1):93–134, 2001. 68. B RYANT, R. E. und M. N. V ELEV: Veriﬁcation of Pipelined Microprocessors by Com- paring Memory Execution Sequences in Symbolic Simulation. In: Proceedings of the Asian Computing Science Conference on Advances in Computing Science (ASIAN), Sei- ten 18–31, 1997.
Literatur 565 69. B UCK , J., S. H A, E. A. L EE und D. G. M ESSERSCHMITT: Ptolemy: A Framework for Simulating and Prototyping Heterogeneous Systems. International Journal on Computer Simulation, 4(2):155–182, 1994. 70. B UCK , J. T.: Scheduling Dynamic Dataﬂow Graphs with Bounded Memory Using the Token Flow Model. Doktorarbeit, Dept. of EECS, UC Berkeley, Berkeley, CA 94720, U.S.A., 1993. 71. B URCH , J. R.: Techniques for Verifying Superscalar Microprocessors. In: Proceedings of the Design Automation Conference (DAC), Seiten 552–557, 1996. 72. B URCH , J. R., E. M. C LARKE und D. E. L ONG: Symbolic Model Checking with Par- titioned Transition Relations. In: Proceedings of the International Conference on Very Large Scale Integration (VLSI), Seiten 49–58, 1991. 73. B URCH ., J. R., E. M. C LARKE, D. E. L ONG, K. L. M C M ILLAN und D. L. D ILL: Symbolic Model Checking for Sequential Circuit Veriﬁcation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401–424, 1994. 74. B URCH , J. R., E. M. C LARKE, K. L. M C M ILLAN, D. L. D ILL und L. J. H WANG: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of the Symposium on Logic in Computer Science (LICS), Seiten 428–439, 1990. 75. B URCH , J. R. und D. L. D ILL: Automatic Veriﬁcation of Pipelined Microprocessor Control. In: Proceedings of the International Conference on Computer Aided Veriﬁcati- on (CAV), Seiten 68–80, 1994. 76. B USHNELL , M. und V. AGRAWAL: Essentials of Electronic Testing for Digital, Memory, and Mixed-Signal VLSI Circuits. Kluwer Academic Publishers, Norwell, Massachusetts, U.S.A., 2000. 77. B USTAN , D., D. F ISMAN und J. H AVLICEK: Automata Construction for PSL. Techni- scher Bericht, The Weizmann Institute of Science, 2005. Technical Report MCS05-04. 78. B UTTAZZO , G.: Rate Monotonic vs. EDF: Judgment Day. In: Proceedings of the Inter- national Conference on Embedded Software (EMSOFT), Seiten 67–83, 2003. 79. BUTTAZZO , G.: Hard Real-Time Computing Systems: Predictable Scheduling Algo- rithms and Applications. Springer, New York, NY, U.S.A., 2004. 80. C ABODI , G., P. C AMURATI, L. L AVAGNO und S. Q UER: Disjunctive Partitioning and Partial Iterative Squaring: An Effective Approach for Symbolic Traversal of Large Cir- cuits. In: Proceedings of the Design Automation Conference (DAC), Seiten 728–733, 1997. 81. C ABODI , G., P. C AMURATI und S. Q UER: Improved Reachability Analysis of Large Finite State Machines. In: Proceedings of the International Conference on Computer- Aided Design (ICCAD), Seiten 354–360, 1996. 82. C ADAR , C., V. G ANESH, P. M. PAWLOWSKI, D. L. D ILL und D. R. E NGLER: EXE: Automatically Generating Inputs of Death. In: Proceedings of the Conference on Com- puter and Communications Security (CCS), Seiten 322–335, 2006. 83. C ARLONI , L. P., K. L. M C M ILLAN, A. S ALDANHA und A. L. S ANGIOVANNI - V INCENTELLI: A Methodology for Correct-by-Construction Latency Insensitive Design. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 309–315, 1999. 84. C ARLONI , L. P., K. L M C M ILLAN und A. L. S ANGIOVANNI -V INCENTELLI: Theory of Latency-Insensitive Design. IEEE Transactions on Computer-Aided Design of Inte- grated Circuits and Systems, 20(9):1059–1076, 2001. 85. C ARLONI , L. P. und A. L. S ANGIOVANNI -V INCENTELLI: Performance Analysis and Optimization of Latency Insensitive Systems. In: Proceedings of the Design Automation Conference (DAC), Seiten 361–367, 2000.
566 Literatur 86. C ARTER , W. C., W. H. J OYNER und D. B RAND: Symbolic simulation for correct ma- chine design. In: Proceedings of the Design Automation Conference (DAC), Seiten 280– 286, 1979. 87. C ASSANDRAS , C. G. und S. L AFORTUNE: Introduction to Discrete Event Systems. Springer, New York, NY, U.S.A., 1999. 88. C ASSEZ , F. und O.-H. ROUX : Structural Translation from Time Petri Nets to Timed Automata. Electronic Notes in Theoretical Computer Science, 128(6):145–160, 2005. 89. C HAKI , S., E. M. C LARKE, J. O UAKNINE, N. S HARYGINA und N. S INHA: State/ Event-Based Software Model Checking. In: In Proceeding of the International Confe- rence on Integrated Formal Methods, Seiten 128–147, 2004. 90. C HETTO , H., M. S ILLY und T. B OUCHENTOUF : Dynamic Scheduling of Real-Time Tasks under Precedence Constraints. Real-Time Systems, 2:325–346, 1990. 91. C HUSHO , T.: Test Data Selection and Quality Estimation Based on the Concept of Es- sential Branches for Path Testing. IEEE Transactions on Software Engineering, SE- 13(5):509–517, 1987. 92. C IESIELSKI , M., P. K ALLA und S. A SKAR: Taylor Expansion Diagrams: A Canonical Representation for Veriﬁcation of Data Flow Designs. IEEE Transactions on Computers, 55(9):1188–1201, 2006. 93. C IESIELSKI , M., P. K ALLA, Z. Z ENG und B. ROUZEYRE: Taylor Expansion Diagrams: A New Representation for RTL Veriﬁcation. In: Proceedings of the High-Level Design Validation and Test Workshop (HLDVT), Seiten 70–75, 2001. 94. C IESIELSKI , M., P. K ALLA, Z. Z HENG und B. ROUZEYRE: Taylor Expansion Dia- grams: A Compact, Canonical Representation with Applications to Symbolic Veriﬁca- tion. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 285–289, 2002. ˚ 95. C LAESSEN , K. und J. M ARTENSSON: An Operational Semantics for Weak PSL. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), Seiten 337–351, 2004. ´ 96. C LARIS O , R. und J. C ORTADELLA : The Octahedron Abstract Domain. Science of Computer Programming, 64(1):115–139, 2006. 97. C LARKE , E. M. und E. A. E MERSON: Design and Synthesis of Synchronization Skele- tons Using Branching-Time Temporal Logic. In: Processings of the Workshop on Logic of Programs, Seiten 52–71, 1982. 98. C LARKE , E. M., E. A. E MERSON und A. P. S ISTLA : Automatic Veriﬁcation of Finite- State Concurrent Systems Using Temporal Logic Speciﬁcations. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986. 99. C LARKE , E. M., M. F UJITA, P. M C G EER, K. L. M C M ILLAN, J. YANG und X. Z HAO: Multi-Terminal Binary Decision Diagrams: An Efﬁcient Data Structure for Matrix Re- presentation. In: Proceedings of the International Workshop on Logic Synthesis (IWLS), Seiten 1–15, 1993. 100. C LARKE , E. M., O. G RUMBERG, S. J HA, Y. L U und H. V EITH: Counterexample- Guided Abstraction Reﬁnement for Symbolic Model Checking. Journal of the ACM, 50(5):752–794, 2003. 101. C LARKE , E. M., O. G RUMBERG und D. E. L ONG : Model Checking and Abstraction. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 343–354, 1992. 102. C LARKE , E. M., D. K ROENING und F. L ERDA: A Tool for Checking ANSI-C Programs. In: Proceedings of the International Conference on Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS), Seiten 168–176, 2004.
Literatur 567 103. C LARKE , E. M., D. K ROENING, N. S HARYGINA und K. YORAV: Predicate Abstrac- tion of ANSI-C Programs Using SAT. Journal of Formal Methods in System Design, 25(2–3):105–127, 2004. 104. C LARKE , E. M., D. K ROENING und K. Y ORAV: Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. In: Proceedings of the Design Au- tomation Conference (DAC), Seiten 368–371, 2003. 105. C LARKE , E. M., D. K ROENING und K. YORAV : Specifying and Verifying Systems with Multiple Clocks. In: Proceedings of the International Conference on Computer Design (ICCD), Seiten 48–55, 2003. 106. C LARKE , E. M., K. L. M C M ILLAN, X. Z HAO, M. F UJITA und J. YANG: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. In: Proceedings of the Design Automation Conference (DAC), Seiten 54–60, 1993. 107. C LARKE , E. M., O.G RUMBERG und D. A. P ELED: Model Checking. MIT Press, Cam- bridge, MA, U.S.A., 1999. 108. C LARKE , L. A., J. H ASSELL und D. J. R ICHARDSON: A Close Look at Domain Testing. IEEE Transactions on Software Engineering, 8(4):380–390, 1982. 109. C LARKE , L. A., A. P ODGURSKI, D. J. R ICHARDSON und S. J. Z EIL: A Comparison of Data Flow Path Selection Criteria. In: Proceedings of the International Conference on Software Engineering (ICSE), Seiten 28–30, 1985. 110. C OCHET-T ERRASSON , J., G. C OHEN, S. G AUBERT , M. M C G ETTRICK und J.-P. Q UADRAT: Numerical Computation of Spectral Elements in Max-Plus Algebra. In: Pro- ceedings of the Conference on System Structure and Control, Seiten 667–674, 1998. 111. C OELHO J R ., C. N. und H. D. F OSTER: Assertion-Based Veriﬁcation – Property Spe- ciﬁcation. In: Advanced Formal Veriﬁcation, Seiten 167–204. Kluwer Academic Publis- hers, Boston, 2004. 112. C OHEN , G., D. D UBOIS, J. Q UADRAT und M. V IOT: A Linear-System-Theoretic View of Discrete-Event Processes and its Use for Performance Evaluation in Manufacturing. IEEE Transactions on Automatic Control, 30(3):210–220, 1985. 113. C OMMONER , F., A. W. H OLT, S. E VEN und A. P NUELI: Marked Directed Graphs. Journal of Computer and System Sciences, 5:511–523, 1971. 114. C OOK , B., D. K ROENING und N. S HARYGINA: Cogent: Accurate Theorem Proving for Program Veriﬁcation. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 296–300, 2005. 115. C OOK , B., D. K ROENING und N. S HARYGINA: Symbolic Model Checking for Asyn- chronous Boolean Programs. In: Proceedings of the International SPIN Workshop (SPIN), Seiten 75–90, 2005. 116. C OOK , S. A.: The Complexity of Theorem-Proving Procedures. In: Proceedings of the Symposium on Theory of Computing (STOC), Seiten 151–158, 1971. 117. C OUDERT, O., C. B ERTHET und J. C. M ADRE: Veriﬁcation of Synchronous Sequential Machines Based on Symbolic Execution. In: Proceedings of the International Workshop on Automatic Veriﬁcation Methods for Finite State Systems, Seiten 365–373, 1990. 118. C OUSOT, P. und R. C OUSOT: Abstract Interpretation: A Uniﬁed Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 238–252, 1977. 119. C OUSOT, P. und R. C OUSOT: Systematic Design of Program Analysis Frameworks. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 269–282, 1979.
568 Literatur 120. C OUSOT, P. und N. H ALBWACHS : Automatic Discovery of Linear Restraints Among Va- riables of a Program. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 84–96, 1978. 121. C RUZ , R. L.: A Calculus for Network Delay, Part I: Network Elements in Isolation. IEEE Transactions on Information Theory, 37(1):114–131, 1991. 122. C URRIE , D. W., X. F ENG, M. F UJITA, A. J. H U, M. K WAN und S. R AJAN: Embedded Software Veriﬁcation Using Symbolic Execution and Uninterpreted Functions. Interna- tional Journal of Parallel Programming, 34(1):61–91, 2006. 123. C URRIE , D. W., A. J. H U, S. R AJAN und M. F UJITA: Automatic Formal Veriﬁcation of DSP Software. In: Proceedings of the Design Automation Conference (DAC), Seiten 130–135, 2000. ¨ 124. C YRLUK , D., O. M OLLER und H. RUESS: An Efﬁcient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 60–71, 1997. 125. C YTRON , R., J. F ERRANTE, B. K. ROSEN, M. N. W EGMAN und F. K. Z ADECK : Efﬁ- ciently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Transactions on Programming Languages and Systems (TOPLAS), 13(4):451– 490, 1991. 126. DAHAN , A., D. G EIST, L. G LUHOVSKY, D. P IDAN, G. S HAPIR , Y. W OLFSTHAL, L. B ENALYCHERIF, R. K AMIDEM und Y. L AHBIB : Combining System Level Modeling with Assertion Based Veriﬁcation. In: Proceedings of the International Symposium on Quality of Electronic Design (ISQED), Seiten 310–315, 2005. 127. DANIELE , M., F. G IUNCHIGLIA und M. Y. VARDI: Improved Automata Generation for Linear Temporal Logic. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 249–260, 1999. 128. DAVIS , M., G. L OGEMANN und D. L OVELAND: A Machine Program for Theorem- Proving. Communications of the ACM, 5(7):394–397, 1962. 129. DAVIS , M. und H. P UTNAM: A Computing Procedure for Quantiﬁcation Theory. Jour- nal of the ACM, 7(3):201–215, 1960. 130. D EHARBE , D. und S. R ANISE : Light-Weight Theorem Proving for Debugging and Ve- rifying Units of Code. In: Proceedings of the Conference on Software Engineering and Formal Methods, Seiten 220–228, 2003. 131. D ETLEFS , D., G. N ELSON und J. B. S AXE: Simplify: A Theorem Prover for Program Checking. Journal of the ACM, 52(3):365–473, 2005. 132. D ILL , D. L.: Timing Assumptions and Veriﬁcation of Finite-State Concurrent Systems. In: Proceedings of the International Workshop on Automatic Veriﬁcation Methods for Finite State Systems, Seiten 197–212, 1990. 133. D ONLIN , A.: Transaction Level Modeling: Flows and Use Models. In: Proceedings of the Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), Seiten 75–80, 2004. 134. D RECHSLER , R. und B. B ECKER: Overview of Decision Diagrams. IEE Proceedings on Computers and Digital Techniques, 144(3):187–193, 1997. 135. D RECHSLER , R. und B. B ECKER: Binary Decision Diagrams – Theory and Implemen- tation. Kluwer Academic Publishers, Dordrecht, The Netherlands, 1998. 136. D RECHSLER , R., B. B ECKER und S. RUPPERTZ: K*BMDs: A New Data Structure for Veriﬁcation. In: Proceedings of the European Conference on Design and Test (EDTC), Seiten 2–8, 1996. ¨ ¨ 137. D RECHSLER , R., S. E GGERSGL USS, G. F EY, J. S CHL OFFEL und D. T ILLE: Efﬁziente Erf¨ llbarkeitsalgorithmen f¨ r die Generierung von Testmustern. it – information tech- u u nology, 51(2):102–111, 2009.
Literatur 569 138. D RECHSLER , R., A. S ARABI, M. T HEOBALD, B. B ECKER und M. A. P ERKOWSKI : Efﬁcient Representation and Manipulation of Switching Functions Based on Ordered Kronecker Functional Decision Diagrams. In: Proceedings of the Design Automation Conference (DAC), Seiten 415–419, 1994. 139. D RECHSLER , R., M. T HEOBALD und B. B ECKER: Fast OFDD based Minimization of Fixed Polarity Reed-Muller Expressions. In: Proceedings of the European Conference on Design Automation (ECDA), Seiten 2–7, 1994. 140. D’S ILVA , V., D. K ROENING und G. W EISSENBACHER: A Survey of Automated Tech- niques for Formal Software Veriﬁcation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7):1165–1178, 2008. 141. D UBOIS , O., P. A NDRE, Y. B OUFKHAD und J. C ARLIER: SAT versus UNSAT. In: J OHNSON , D. S. und M. A. T RICK (Herausgeber): Second DIMACS Implementation Challenge, Band 26 der Reihe Series in Discrete Mathematics and Theoretical Computer Science (DIMACS), Seiten 415–434. American Mathematical Society, 1996. 142. D UTERTRE , B. und L. DE M OURA: A Fast Linear-Arithmetic Solver for DPLL(T). In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 81–94, 2006. 143. E CKER , W., V. E SEN, T. S TEININGER , M. V ELTEN und M. H ULL: Execution Seman- tics and Formalisms for Multi-Abstraction TLM Assertions. In: Proceedings of the In- ternational Conference on Formal Methods and Models for Co-Design (MEMOCODE), Seiten 93–102, 2006. 144. E CKER , W., V. E SEN, T. S TEININGER , M. V ELTEN und M. H ULL: Implementation of a Transaction Level Assertion Framework in SystemC. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 1–6, 2007. 145. E IJK , C. A. J. VAN: Formal Methods for the Veriﬁcation of Digital Circuits. Doktorar- beit, Eindhoven University of Technology, The Netherlands, 1997. 146. E IJK , C. A. J. VAN: Sequential Equivalence Checking based on Structural Similari- ties. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 19(7):814–819, 2000. 147. E KER , J., J. W. JANNECK , E. A. L EE , J. L IU , X. L IU, J. L UDVIG, S. N EUENDORFFER, S. S ACHS und Y. X IONG: Taming Heterogeneity – the Ptolemy Approach. Proceedings of the IEEE, 91(1):127–144, 2003. 148. E MERSON , E. A.: Temporal and Modal Logic. In: Formal Models and Semantics, Band B der Reihe Handbook of Theoretical Computer Science, Seiten 995–1072. MIT Press, Cambridge, MA, U.S.A., 1990. 149. E MERSON , E. A. und E. M. C LARKE: Characterizing Correctness Properties of Par- allel Programs Using Fixpoints. In: Proceedings of the Colloquium on Automata, Lan- guages and Programming, Seiten 169–181, 1980. 150. E MERSON , E. A. und J. Y. H ALPERN: ”Sometimes” and ”Not Never” Revisited: On Branching versus Linear Time. In: Proceedings of the Symposium on Principles of Pro- gramming Languages (POPL), Seiten 127–140, 1983. 151. E MERSON , E. A., A. K. M OK, A. P. S ISTLA und J. S RINIVASAN: Quantitative Tem- poral Reasoning. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 136–145, 1990. 152. E MERSON , E. A. und R. J. T REFLER: Parametric Quantitative Temporal Reasoning. In: Proceedings of the Symposium on Logic in Computer Science (LICS), Seiten 336– 343, 1999. 153. E NGELS , M., G. B ILSEN, R. L AUWEREINS und J. P EPERSTRAETE : Cyclo-Static Da- ta Flow: Model and Implementation. In: Proceedings of the Asilomar Conference on Signals, Systems, and Computers, Seiten 503–507, 1994.
570 Literatur 154. E RNST, R. und W. Y E: Embedded Program Timing Analysis Based on Path Clustering and Architecture Classiﬁcation. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 598–604, 1997. 155. E SPARZA , J.: Model Checking Using Net Unfoldings. In: Proceedings of the Conference on Theory and Practice of Software Development (TAPSOFT), Seiten 613–628, 1993. 156. E VANS , A., A. S ILBURT, G. V RCKOVNIK, T. B ROWN, M. D UFRESNE, G. H ALL, T. H O und Y. L IU: Functional Veriﬁcation of Large ASICs. In: Proceedings of the Design Automation Conference (DAC), Seiten 650–655, 1998. 157. FALK , J., C. H AUBELT und J. T EICH: Efﬁcient Representation and Simulation of Model-Based Designs in SystemC. In: Proceedings of the Forum on Design Langua- ges (FDL), Seiten 129–134, 2006. 158. F EAUTRIER , P.: Array Expansion. In: Proceedings of the International Conference on Supercomputing (ICS), Seiten 429–441, 1988. 159. F ENG , X. und A. J. H U: Automatic Formal Veriﬁcation for Scheduled VLIW Code. In: Proceedings of the Conference on Languages, Compilers and Tools for Embedded Systems (SCOPES), Seiten 85–92, 2002. 160. F ENG , X. und A. J. H U: Cutpoints for Formal Equivalence Veriﬁcation of Embedded Software. In: Proceedings of the International Conference on Embedded Software (EM- SOFT), Seiten 307–316, 2005. 161. F ENG , X. und A. J. H U: Early Cutpoint Insertion for High-Level Software vs. RTL For- mal Combinational Equivalence Veriﬁcation. In: Proceedings of the Design Automation Conference (DAC), Seiten 1063–1068, 2006. ¨ 162. F ETTWEIS , A.: Realizability of Digital Filter Networks. Archiv Elek. Ubertragung, 30(2):90–96, 1976. 163. F EY, G., R. D RECHSLER und M. C IESIELSKI: Algorithms for Taylor Expansion Dia- grams. In: Proceedings of the International Symposium on Multiple-Valued Logic (ISMVL), Seiten 235–240, 2004. 164. F LANAGAN , C., R. J OSHI, X. O U und J. B. S AXE: Theorem Proving Using Lazy Proof Explication. In: Proceedings of the International Conference on Computer Aided Veriﬁ- cation (CAV), Seiten 355–367, 2003. 165. http://www.ﬂexray.com. 166. F LOYD , R. W.: Assigning Meaning to Programs. In: Proceedings of the Symposium of Applied Mathematics, Seiten 19–32, 1967. 167. http://www.haifa.ibm.com/projects/veriﬁcation/focs/. 168. F OSTER , H. D., A. C. K ROLNIK und D. J. L ACEY: Assertion-Based Design. Kluwer Academic Publishers, Dordrecht, The Netherlands, 2004. 2. Auﬂage. 169. F OWLER , M. und K. S COTT: UML Distilled: Applying the Standard Object Modeling Language. Addison-Wesley, Reading, MA, U.S.A., 1997. 170. G AJSKI , D. D. und R. H. K UHN : New VLSI Tools. IEEE Computer, 16(12):11–14, 1983. 171. G AJSKI , D. D., F. VAHID, S. NARAYAN und J. G ONG: Speciﬁcation and Design of Embedded Systems. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1994. ¨ 172. G AJSKI , D. D., J. Z HU, R. D OMER, A. G ERSTLAUER und S. Z HAO: SpecC: Speciﬁ- cation Language and Design Methodology. Kluwer Academic Publishers, 2000. 173. G ANAI , M. K. und A. A ZIZ: Improved SAT-Based Bounded Reachability Analysis. In: Proceedings of the Asia and South Paciﬁc Design Automation Conference (ASPDAC), Seiten 729–734, 2002. 174. G ANAI , M. K. und A. G UPTA: SAT-based Scalable Formal Veriﬁcation Solutions. Springer, New York, NY, U.S.A., 2007.
Literatur 571 175. G ANAI , M. K., A. G UPTA und P. A SHAR: Efﬁcient Modeling of Embedded Memories in Bounded Model Checking. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 440–452, 2004. 176. G ANAI , M. K., A. G UPTA und P. A SHAR: Beyond Safety: Customized SAT-Based Mo- del Checking. In: Proceedings of the Design Automation Conference (DAC), Seiten 738–743, 2005. 177. G ANAI , M. K., A. G UPTA und P. A SHAR: Veriﬁcation of Embedded Memory Systems using Efﬁcient Memory Modeling. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 1096–1101, 2005. 178. G ANAI , M. K., M. TALUPUR und A. G UPTA : SDSAT: Tight Integration of Small Do- main Encoding and Lazy Approaches in a Separation Logic Solver. In: Tools and Algo- rithms for the Construction and Analysis of Systems, Seiten 135–150. Springer, Berlin, Heidelberg, 2006. 179. G ANESH , V. und D. L. D ILL: A Decision Procedure for Bit-Vectors and Arrays. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 524–536, 2007. 180. G AREY, M. R. und D. S. J OHNSON : Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, New York, NY, U.S.A., 1979. 181. G ASTIN , P. und D. O DDOUX: Fast LTL to B¨ chi Automata Translation. In: Proceedings u of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 53–65, 2001. 182. G ERSTLAUER , A., C. H AUBELT, A. D. P IMENTEL, T. P. S TEFANOV, D. D. G AJSKI und J. T EICH: Electronic System-Level Synthesis Methodologies. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 28(10):1517–1530, 2009. 183. G ERTH , R., D. P ELED, M. Y. VARDI und P. W OLPER: Simple On-the-Fly Automatic Veriﬁcation of Linear Temporal Logic. In: Proceedings of the International Symposium on Protocol Speciﬁcation, Testing and Veriﬁcation, Seiten 3–18, 1996. 184. G HAMARIAN , A. H.: Timing Analysis of Synchronous Data Flow Graphs. Doktorarbeit, Eindhoven University of Technology, The Netherlands, 2008. 185. G HAMARIAN , A. H., M. C. W. G EILEN, S. S TUIJK, T. BASTEN , A. J. M. M OONEN, M. J. G. B EKOOIJ, B. D. T HEELEN und M. R. M OUSAVI: Throughput Analysis of Synchronous Data Flow Graphs. In: Proceedings of the International Conference on Application of Concurrency to System Design (ACSD), Seiten 25–36, 2006. 186. G HAMARIAN , A. H., S. S TUIJK, T. BASTEN, M. C. W. G EILEN und B. D. T HEELEN: Latency Minimization for Synchronous Data Flow Graphs. In: Proceedings of the Eu- romicro Conference on Digital System Design Architectures, Methods and Tools (DSD), Seiten 189–196, 2007. 187. G HEORGHITA , S. V. und R. G RIGORE: Constructing Checkers from PSL Properties. In: In Proceedings of the International Conference on Control Systems and Computer Science, Seiten 757–762, 2005. 188. G IANNAKOPOULOU , D. und F. L ERDA: From States to Transitions: Improving Trans- lation of LTL Formulae to B¨ chi Automata. In: Proceedings of the International Con- u ference on Formal Techniques for Networked and Distributed Systems (FORTE), Seiten 308–326, 2002. 189. G IRAULT, C. und R. VALK: Petri Nets for Systems Engineering – A Guide to Modeling, Veriﬁcation, and Application. Springer, Berlin, Heidelberg, New York, 2003. 190. G IRGIS , M. und M. W OODWARD: An Experimental Comparison of the Error Expo- sing Ability of Program Testing Criteria. In: Proceedings of the Workshop on Software Testing, Seiten 64–73, 1986.
572 Literatur 191. G LADIGAU , J., F. B LENDINGER, C. H AUBELT und J. T EICH: Symbolische Modell- pr¨ fung Aktor-orientierter High-level SystemC-Modelle mit Intervalldiagrammen. In: u Methoden und Beschreibungssprachen zur Modellierung und Veriﬁkation von Schaltun- gen und Systemen, Seiten 109–118, 2008. 192. G LADIGAU , J., C. H AUBELT und J. T EICH: Symbolic Scheduling of SystemC Dataﬂow Designs. In: Languages for Embedded Systems and their Applications, Band 36 der Reihe Lecture Notes in Electrical Engineering, Seiten 183–199. Springer, 2009. 193. G LADIGAU , J ENS: Symbolische Ablaufplanung von SysteMoC-Beschreibungen. Di- plomarbeit, Department of Computer Science, University of Erlangen-Nuremberg, 2006. 194. G ODEFROID , P.: Partial-Order Methods for the Veriﬁcation of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, New York, NY, U.S.A., 1996. 195. G ODEFROID , P.: Model Checking for Programming Languages Using VeriSoft. In: Pro- ceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 174–186, 1997. 196. G ODEFROID , P. und P. W OLPER : A Partial Approach to Model Checking. In: Procee- dings of the Symposium on Logic in Computer Science (LICS), Seiten 406–415, 1991. 197. G ODEFROID , P. und P. W OLPER: Using Partial Orders for the Efﬁcient Veriﬁcation of Deadlock Freedom and Safety Properties. Journal of Formal Methods in System Design, 2(2):149–164, 1993. ¨ ¨ 198. G ODEL , K URT: Uber formal unentscheidbare S¨ tze der Principia Mathematica und a verwandter Systeme I. Monatshefte f¨ r Mathematik und Physik, 38:173–198, 1931. u 199. G OEL , A. und R. E. B RYANT: Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 10816–10821, 2003. 200. G OEL , A., K. S AJID, H. Z HOU , A. A ZIZ und V. S INGHAL: BDD Based Procedures for a Theory of Equality with Uninterpreted Functions. Journal of Formal Methods in System Design, 22(3):205–224, 2003. 201. G OLDBERG , E. und Y. N OVIKOV: BerkMin: A Fast and Robust SAT-solver. In: Procee- dings of the Design, Automation and Test in Europe (DATE), Seiten 142–149, 2002. 202. G OMEZ -P RADO , D., Q. R EN, S. A SKAR, M. C IESIELSKI und E. B OUTILLON: Varia- ble Ordering for Taylor Expansion Diagrams. In: Proceedings of the High-Level Design Validation and Test Workshop (HLDVT), Seiten 55–59, 2004. 203. G ORDON , M., J OE H URD und K. S LIND: Executing the Formal Semantics of the Accel- lera Property Speciﬁcation Language by Mechanised Theorem Proving. In: Proceedings of the Conference on Correct Hardware Design and Veriﬁcation Methods, Seiten 200– 215, 2003. 204. G OVINDARAJAN , R. und G. R. G AO : Rate-Optimal Schedule for Multi-Rate DSP Com- putations. Journal of VLSI Signal Processing Systems, 9(3):211–232, 1995. 205. G RAF, S. und H. S A¨DI: Construction of Abstract State Graphs with PVS. In: Pro- I ceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 72–83, 1997. 206. G ROSSE , D. und R. D RECHSLER : Ein Ansatz zur formalen Veriﬁkation von Schaltungs- beschreibungen in SystemC. it - Information Technology, 45(4):219–226, 2003. ¨ 207. G R OTKER , T., S. L IAO, G. M ARTIN und S. S WAN: System Design with SystemC. Klu- wer Academic Publishers, Norwell, Massachusetts, Dordrecht, 2002. 208. G UPTA , A. und P. A SHAR: Integrating a Boolean Satisﬁability Checker and BDDs for Combinational Equivalence Checking. In: Proceedings of the International Conference on VLSI Design (VLSID), Seiten 222–225, 1998.
Literatur 573 209. G UPTA , A., M. G ANAI, Z. YANG und P. A SHAR: Iterative Abstraction using SAT- based BMC with Proof Analysis. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 416–423, 2003. 210. H ABIBI , A. und S. TAHAR: Design and Veriﬁcation of SystemC Transaction-Level Mo- dels. IEEE Transactions on Very Large Scale Integrated Systems, 14(1):57–68, 2006. 211. H ACHTEL , G. D. und F. S OMENZI: Logic Synthesis and Veriﬁcation Algorithms. Klu- wer Academic Publishers, Norwell, Massachusetts 02061 U.S.A., 1996. 212. H ALBWACHS , N., P. C ASPI, P. R AYMOND und D. P ILAUD: The Synchronous Data Flow Programming Language LUSTRE. Proceedings of the IEEE, 79(9):1305–1320, 1991. 213. H ALBWACHS , N., Y.-E. P ROY und P. ROUMANOFF: Veriﬁcation of Real-Time Sys- tems using Linear Relation Analysis. Journal of Formal Methods in System Design, 11(2):157–185, 1997. 214. H AMAGUCHI , K., A. M ORITA und S. YAJIMA: Efﬁcient Construction of Binary Mo- ment Diagrams for Verifying Arithmetic Circuits. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 78–82, 1995. ¨ 215. H AUBELT, C., J. FALK, J. K EINERT, T. S CHLICHTER, M. S TREUB UHR, A. D EYHLE, A. H ADERT und J. T EICH: A SystemC-based Design Methodology for Digital Signal Processing Systems. EURASIP Journal on Embedded Systems, Special Issue on Em- bedded Digital Signal Processing Systems, 2007. 216. H AUBELT, C., M. M EREDITH, T. S CHLICHTER und J. K EINERT : SystemCoDesigner: Automatic Design Space Exploration and Rapid Prototyping from Behavioral Models. In: Proceedings of the Design Automation Conference (DAC), Seiten 580–585, 2008. 217. H ENIA , R., A. H AMANN, M. J ERSAK, R. R ACU, K. R ICHTER und R. E RNST: System Level Performance Analysis – The SymTA/S Approach. IEE Proceedings on Computers and Digital Techniques, 152(2):148–166, 2005. 218. H ENZINGER , T. A., X. N ICOLLIN, J. S IFAKIS und S. YOVINE: Symbolic Model Checking for Real-Time Systems. Information and Computation, 111(2):193–244, 1994. 219. H ERBER , P., J. F ELLMUTH und S. G LESNER: Model Checking SystemC Designs Using Timed Automata. In: Proceedings of the Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), Seiten 131–136, 2008. 220. H IND , M.: Pointer Analysis: Haven’t We Solved this Problem Yet? In: Proceedings of the Workshop on Program Analysis for Software Tools and Engineering (PASTE), Seiten 54–61, 2001. 221. H OARE , C. A. R.: An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10):576–580, 1969. 222. H OLZMANN , G. J.: The Model Checker SPIN. IEEE Transactions on Software Engi- neering, 23(5):279–295, 1997. 223. H OPCROFT, J. E., R. M OTWANI und J. D. U LLMAN: Einf¨ hrung in die Automaten- u theorie, Formale Sprachen und Komplexit¨ tstheorie. Pearson Studium, Deutschland, a M¨ nchen, 2002. 2. Auﬂage. u ¨ 224. H ORETH , S. und R. D RECHSLER : Formal Veriﬁcation of Word-Level Speciﬁcations. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 52–58, 1999. 225. H ORN , W. A.: Some Simple Scheduling Algorithms. Naval Research Logistics Quarter- ly, 21:177–185, 1974. 226. H ORWITZ , S., T. R EPS und D. B INKLEY: Interprocedural Slicing Using Dependence Graphs. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI), Seiten 35–46, 1988. 227. H OWDEN , W. E.: Theoretical and Empirical Studies of Program Testing. IEEE Tran- sactions on Software Engineering, SE-4(4):293–298, 1978.
574 Literatur 228. H OWDEN , W. E.: Theoretical and Empirical Studies of Program Testing. In: Procee- dings of the International Conference on Software Engineering (ICSE), Seiten 305–311, 1978. 229. H U , A. J.: High-Level vs. RTL Combinational Equivalence: An Introduction. In: Pro- ceedings of the International Conference on Computer Design (ICCD), Seiten 274–279, 2007. 230. H UANG , C.-Y. und K.-T. C HENG: Assertion Checking by Combined Word-Level ATPG and Modular Arithmetic Constraint-Solving Techniques. In: Proceedings of the Design Automation Conference (DAC), Seiten 118–123, 2000. 231. I BARRA , O. H. und S. M ORAN: Probabilistic Algorithms for Deciding Equivalence of Straight-Line Programs. Journal of the ACM, 30(1):217–228, 1983. 232. IEEE: IEEE Standard Glossary of Software Engineering Terminology. IEEE Std 610.12-1990, 1990. 233. IEEE: IEEE Standard VHDL Language Reference Manual. IEEE Std. 1076-1993, 1993. 234. IEEE: IEEE Standard for Property Speciﬁcation Language (PSL). IEEE Std 1850, 2005. 235. IEEE: IEEE Standard for SystemVerilog – Uniﬁed Hardware Design, Speciﬁcation, and Veriﬁcation Language. IEEE Std 1800, 2005. 236. IEEE: IEEE Standard SystemC Language Reference Manual. IEEE Std 1666, 2006. 237. http://www.cadence.com/products/fv/design team simulator/. 238. http://www.cadence.com/products/fv/formal veriﬁer/. 239. I SHIURA , N., H. S AWADA und S. YAJIMA: Minimization of Binary Decision Diagrams based on Exchanges of Variables. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 472–475, 1991. 240. ITRS: International Technology Roadmap for Semiconductors – System Drivers. Tech- nischer Bericht, ITRS, 2007. http://www.itrs.net/. ˇ ´ 241. I VAN CI C , F., I. S HLYAKHTER , A. G UPTA, M. K. G ANAI , V. K AHLON, C. WANG und Z. YANG: Model Checking C Programs using F-Soft. In: Proceedings of the Internatio- nal Conference on Computer Design (ICCD), Seiten 297–308, 2005. ˇ ´ 242. I VAN CI C , F., Z. YANG, M. K. G ANAI , A. G UPTA und P. A SHAR: Efﬁcient SAT-Based Bounded Model Checking for Software Veriﬁcation. Theoretical Computer Science, 404(3):256–274, 2008. 243. JACKSON , J. R.: Scheduling a Production Line to Minimize Maximum Tardiness. Tech- nischer Bericht 43, University of California, Los Angeles, 1955. 244. JAIN , H., D. K ROENING und E. M. C LARKE: Veriﬁcation of SpecC Using Predicate Abstraction. In: Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE), Seiten 7–16, 2004. 245. JAIN , J., A. NARAYAN, C. C OELHO, S. P. K HATRI, A. L. S ANGIOVANNI -V INCEN - TELLI , R. K. B RAYTON und M. F UJITA : Decomposition Techniques for Efﬁcient ROBDD Construction. In: Proceedings of the International Conference on Formal Me- thods in Computer-Aided Design (FMCAD), Seiten 419–434, 1996. 246. JALOTE , P.: Fault Tolerance in Distributed Systems. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1994. 247. J ERSAK , M.: Compositional Performance Analysis for Complex Embedded Applicati- ons. Doktorarbeit, Technische Universit¨ t Braunschweig, Deutschland, 2005. a 248. J ONES , N. D. und S. S. M UCHNICK: Flow Analysis and Optimization of LISP-like Structures. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 244–256, 1979. 249. J OSEPH , M. und P. PANDYA: Finding Response Times in a Real-Time System. The Computer Journal, 29(5):390–395, 1986.
Literatur 575 250. K AHN , G.: The Semantics of a Simple Language for Parallel Programming. In: Procee- dings of the IFIP Congress, Seiten 471–475, Stockholm, Sweden, 1974. 251. K ALLA , P., M. C IESIELSKI, E. B OUTILLON und E. M ARTIN: High-Level Design Veri- ﬁcation Using Taylor Expansion Diagrams: First Results. In: Proceedings of the High- Level Design Validation and Test Workshop (HLDVT), Seiten 13–17, 2002. 252. K ATZ , S. und D. P ELED: Veriﬁcation of Distributed Programs Using Representative Interleaving Sequences. Journal of Distributed Computing, 6(2):107–120, 1992. 253. K EBSCHULL , U., E. S CHUBERT und W. ROSENSTIEL: Multilevel Logic Synthesis ba- sed on Functional Decision Diagrams. In: Proceedings of the European Conference on Design Automation (ECDA), Seiten 43–47, 1992. ¨ 254. K EINERT, J., M. S TREUB UHR, T. S CHLICHTER, J. FALK, J. G LADIGAU, C. H AU - BELT , J. T EICH und M. M EREDITH: SystemCoDesigner - An Automatic ESL Synthesis Approach by Design Space Exploration and Behavioral Synthesis for Streaming Appli- cations. ACM Transactions on Design Automation of Electronic Systems (TODAES), 14(1):1–23, 2009. 255. K ELLY, J. C. und K. K EMP: Formal Methods Speciﬁcation and Veriﬁcation Guide- book for Software and Computer Systems, Volume I: Planning and Technology Insertion. Technischer Bericht NASA-GB-002-95, NASA, Ofﬁce of Safety and Mission Assuran- ce, 1995. 256. K EMPF, T., M. D OERPER, R. L EUPERS, G. A SCHEID, H. M EYR, T. KOGEL und B. VANTHOURNOUT : A Modular Simulation Framework for Spatial and Temporal Task Mapping onto Multi-Processor SoC Platforms. In: Proceedings of the Design, Automa- tion and Test in Europe (DATE), Seiten 876–881, 2005. 257. K ERNIGHAN , B. W. und D. R ITCHIE: The C Programming Language. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1988. 2. Auﬂage. 258. K IENHUIS , B., E. D EPRETTERE, K. V ISSERS und P. VAN DER W OLF: An Approach for Quantitative Analysis of Application-Speciﬁc Dataﬂow Architectures. In: Proceedings of the Conference on Application-Speciﬁc Systems, Architectures and Processors (ASAP), Seiten 338–349, 1997. 259. K INDLER , E. und T. V ESPER : ESTL: A Temporal Logic for Events and States. In: Proceedings of the International Conference on Application and Theory of Petri Nets (ICATPN), Seiten 365–384, 1998. 260. K ING , J. C.: Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385–394, 1976. 261. K IRCHNER , H., S. R ANISE, C. R INGEISSEN und D. K. T RAN: On Superposition- Based Satisﬁability Procedures and Their Combination. In: Proceedings of the Inter- national Conference on Theoretical Aspects of Computing (ICTAC), Seiten 594–608, 2005. 262. K LEIN , M.: A Practitioner’s Handbook for Real-Time Analysis. Kluwer Academic Pu- blishers, Boston, MA, U.S.A., 1993. 263. K LINGERMAN , E. und A. D. S TOYENKO: Real-Time Euclid: A Language for Reliable Real-Time Systems. IEEE Transactions on Software Engineering, SE-12(9):941–949, 1986. 264. KOELBL , A., Y. L U und A. M ATHUR : Embedded Tutorial: Formal Equivalence Checking Between System-Level Models and RTL. In: Proceedings of the Internatio- nal Conference on Computer-Aided Design (ICCAD), Seiten 965–971, 2005. 265. KONDRATYEV, A., M. K ISHINEVSKY, A. TAUBIN und S. T EN: A Structural Approach for the Analysis of Petri Nets by Reduced Unfoldings. In: Proceedings of the Conference on Application and Theory of Petri Nets, Seiten 346–365, 1996.
576 Literatur 266. KOPETZ , H.: Real-Time Systems – Design Principles for Distributed Embedded Appli- cations. Kluwer Academic Publishers, Boston, MA, U.S.A., 1997. 267. KOREN , I. und C. M. K RISHNA: Fault Tolerant Systems. Morgan Kaufmann Publishers Inc., San Francisco, CA, U.S.A., 2007. 268. K RIPKE , S. A.: A Completeness Theorem in Modal Logic. The Journal of Symbolic Logic, 24(1):1–14, 1959. 269. K RIPKE , S. A.: Semantical Considerations on Modal Logic. Acta Philosophica Fennica, 16:83–94, 1963. 270. K ROENING , D. und E. C LARKE: Checking Consistency of C and Verilog Using Pre- dicate Abstraction and Induction. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 66–72, 2004. 271. K ROENING , D. und N. S HARYGINA: Formal Veriﬁcation of SystemC by Automatic Hardware/Software Partitioning. In: Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE), Seiten 101–110, 2005. 272. K ROPF, T HOMAS: Introduction to Formal Hardware Veriﬁcation. Springer, Berlin, Hei- delberg, 1999. 273. K UEHLMANN , A. und F. K ROHM: Equivalence Checking Using Cuts and Heaps. In: Proceedings of the Design Automation Conference (DAC), Seiten 263–268, 1997. 274. K UEHLMANN , A., V. PARUTHI, F. K ROHM und M. K. G ANAI : Robust Boolean Rea- soning for Equivalence Checking and Functional Property Veriﬁcation. IEEE Transacti- ons on Computer-Aided Design of Integrated Circuits and Systems, 21(12):1377–1394, 2002. 275. K UNZ , W., D. K. P RADHAN und S. M. R EDDY: A Novel Framework for Logic Veri- ﬁcation in a Synthesis Environment. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15(1):20–32, 1996. 276. K UNZ , W. und D. S TOFFEL: Reasoning in Boolean Networks. Kluwer Academic Pu- blishers, Dordrecht, The Netherlands, 1997. ¨ 277. K UNZLI , S., F. P OLETTI, L. B ENINI und L. T HIELE: Combining Simulation and For- mal Methods for System-Level Performance Analysis. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 236–241, 2006. 278. L AHBIB , Y., A. P ERRIN , L. M AILLET-C ONTOZ, A. C LOUARD, F. G HENASSIA und R. TOURKI: Enriching the Boolean and the Modeling Layers of PSL with SystemC and TLM Flavors. In: Proceedings of the Forum on Design Languages (FDL), Seiten 273– 278, 2006. 279. L AHIRI , K., A. R AGHUNATHAN und S. D EY: System-Level Performance Analysis for Designing On-Chip Communication Architectures. IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems, 20(6):768–783, Juni 2001. 280. L AHIRI , S. K. und S. A. S ESHIA: The UCLID Decision Procedure. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 475–478, 2004. 281. L AI , Y.-T. und S. S ASTRY: Edge-Valued Binary Decision Diagrams for Multi-Level Hierarchical Veriﬁcation. In: Proceedings of the Design Automation Conference (DAC), Seiten 608–613, 1992. 282. L ALA , P. K.: Fault Tolerant and Fault Testable Hardware Design. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1985. 283. L ALA , P. K. (Herausgeber): Self-Checking and Fault-Tolerant Digital Design. Morgan Kaufmann Publishers Inc., San Francisco, CA, U.S.A., 2001. 284. L AM , W. K.: Hardware Design Veriﬁcation: Simulation and Formal Method-Based Ap- proaches. Pearson Studium, Deutschland, Upper Saddle River, NJ, U.S.A., 2005.
Literatur 577 285. L AMPKA , K., S. P ERATHONER und L. T HIELE: Analytic Real-Time Analysis and Timed Automata: A Hybrid Method for Analyzing Embedded Real-Time Systems. In: Procee- dings of the International Conference on Embedded Software (EMSOFT), Seiten 107– 116, 2009. 286. L AMPORT, L.: ”Sometime” is Sometimes ”Not Never”: On the Temporal Logic of Pro- grams. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 174–185, 1980. 287. L AROUSSINIE , F., N. M ARKEY und P. S CHNOEBELEN: On Model Checking Duratio- nal Kripke Structures. In: Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Seiten 264–279, 2002. 288. L AROUSSINIE , F., P. S CHNOEBELEN, und M. T URUANI: On the Expressivity and Com- plexity of Quantitative Branching-Time Temporal Logics. In: Proceedings of the Latin American Symposium on Theoretical Informatics (LATIN), Seiten 437–446, 2000. 289. L ARRABEE , T.: Test Pattern Generation Using Boolean Satisﬁability. IEEE Transacti- ons on Computer-Aided Design of Integrated Circuits and Systems, 11(1):4–15, 1992. 290. L ASKI , J. W.: On Data Flow Guided Program Testing. ACM SIGPLAN Notices, 17(9):62–71, 1982. 291. L ASKI , J. W. und B. KOREL: A Data Flow Oriented Program Testing Strategy. IEEE Transactions on Software Engineering, SE-9(3):347–354, 1983. 292. L AWLER , E. L.: Optimal Sequencing of a Single Machine Subject to Precedence Cons- traints. Management Science, 19:544–546, 1973. 293. L E B OUDEC , J.Y. und P. T HIRAN: Network Calculus: A Theory of Deterministic Queuing Systems for the Internet. Springer, New York, NY, U.S.A., 2001. 294. L EE , C. Y.: Representation of Switching Circuits by Binary-Decision Programs. Bell Systems Technical Journal, 38:985–999, 1959. 295. L EE , E. A.: Dataﬂow Process Networks. Technischer Bericht UCB/ERL 94/53, Dept. of EECS, UC Berkeley, Berkeley, CA 94720, U.S.A., 1993. 296. L EE , E. A. und D. G. M ESSERSCHMITT: Synchronous Data Flow. Proceedings of the IEEE, 75(9):1235–1245, 1987. 297. L EE , E. A., S. N EUENDORFFER und M. J. W IRTHLIN: Actor-Oriented Design of Em- bedded Hardware and Software Systems. Journal of Circuits, Systems, and Computers, 12(3):231–260, 2003. 298. L EE , E. A. und A. L. S ANGIOVANNI -V INCENTELLI: A Framework for Comparing Models of Computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(12):1217–1229, 1998. 299. L EHOCZKY, J.: Fixed Priority Scheduling of Periodic Task Sets with Arbitrary Dead- lines. In: Proceedings of the Real-Time Systems Symposium (RTSS), Seiten 201–209, 1990. 300. L EHOCZKY, J. P. und L. S HA: Performance of Real-Time Bus Scheduling Algorithms. In: International Conference on Measurement and Modeling of Computer Systems, Sei- ten 44–53, 1986. 301. L EUNG , J. und J. W HITEHEAD: On the Complexity of Fixed Priority Scheduling of Periodic, Real-Time Tasks. Performance Evaluation, 2(4):237–250, 1982. 302. L I , Y.-T. S. und S. M ALIK: Performance Analysis of Embedded Software Using Implicit Path Enumeration. ACM SIGPLAN Notices, 30(11):88–98, 1995. 303. L I , Y.-T. S., S. M ALIK und A. W OLFE: Efﬁcient Microarchitecture Modeling and Path Analysis for Real-Time Software. In: Proceedings of the Real-Time Systems Symposium (RTSS), Seiten 298–307, 1995.
578 Literatur 304. L ICHTENSTEIN , O. und A. P NUELI: Checking that Finite State Concurrent Programs Satisfy their Linear Speciﬁcation. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 97–107, 1985. 305. L IGGESMEYER , P.: Software-Qualit¨ t – Testen, Analysieren und Veriﬁzieren von Soft- a ware. Spektrum Akademischer Verlag, Heidelberg, Berlin, 2002. 306. L IGGESMEYER , P. und D. ROMBACH: Software Egineering eingebetteter Systeme – Grundlagen - Methodik - Anwendungen. Elsevier GmbH, M¨ nchen, 2005. u 307. L IU , C. L. und J. W. L AYLAND: Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment. Journal of the ACM, 20(1):46–61, 1973. 308. L IU , J.: Real-Time Systems. Prentice-Hall, Inc., Boston, MA, U.S.A., 2000. 309. L U , R. und C.-K. KOH : Performance Analysis of Latency-Insensitive Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25(3):469– 483, 2006. 310. M AHFOUDH , M., P. N IEBERT, E. A SARIN und O. M ALER: A Satisﬁability Checker for Difference Logic. In: Proceedings of the Symposium on Theory and Applications of Satisﬁability Testing (SAT), Seiten 222–230, 2002. 311. M ANO , M. M. und C. R. K IME: Logic and Computer Design Fundamentals. Pearson Studium, Deutschland, Upper Saddle River, NJ, U.S.A., 2008. 4. Auﬂage. 312. M ARKEY, N. und P. S CHNOEBELEN: Symbolic Model Checking of Simply-Timed Sys- tems. In: Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systmes (FORMATS), Seiten 102–117, 2004. 313. M ARQUES -S ILVA , J. P.: The Impact of Branching Heuristics in Propositional Satisﬁabi- lity Algorithms. In: Proceedings of the Portuguese Conference on Artiﬁcial Intelligence (EPIA), Seiten 62–74, 1999. 314. M ARQUES -S ILVA , J. P. und K. A. S AKALLAH: GRASP: A Search Algorithm for Pro- positional Satisﬁability. IEEE Transactions on Computers, 48(5):506–521, 1999. 315. M ATSUMOTO , T., H. S AITO und M. F UJITA: Equivalence Checking of C Programs by Locally Performing Symbolic Simulation on Dependence Graphs. In: Proceedings of the International Symposium on Quality of Electronic Design (ISQED), Seiten 370–375, 2006. 316. M C M ILLAN , K. L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Norwell, MA, U.S.A., 1993. 317. M C M ILLAN , K. L.: Using Unfoldings to Avoid the State Explosion Problem in the Veriﬁcation of Asynchronous Circuits. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 164–177, 1993. 318. M C M ILLAN , K. L.: Trace Theoretic Veriﬁcation of Asynchronous Circuits Using Unfol- dings. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 180–195, 1995. 319. M C M ILLAN , K. L.: Veriﬁcation of an Implementation of Tomasulo’s Algorithm by Com- positional Model Checking. In: Proceedings of the International Conference on Com- puter Aided Veriﬁcation (CAV), Seiten 110–121, 1998. 320. M C M ILLAN , K. L.: Interpolation and SAT-Based Model Checking. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 1–13, 2003. 321. M C M ILLAN , K. L. und N. A MLA: Automatic Abstraction without Counterexamples. In: Proceedings of the International Conference on Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS), Seiten 2–17, 2003. 322. M C NAUGHTON , R.: Testing and Generating Inﬁnite Sequences by a Finite Automaton. Information and Control, 9(5):521–530, 1966. 323. M C NAUGHTON , R. und H. YAMADA: Regular Expressions and State Graphs for Auto- mata. IRE Transactions on Electronic Computers, EC-9(1):39–47, 1960.
Literatur 579 324. M EINEL , C. und T. T HEOBALD : Algorithmen und Datenstrukturen im VLSI-Design – OBDD-Grundlagen und -Anwendungen. Springer, Berlin, Heidelberg, 1998. 325. M ELHAM , T.: Abstraction Mechanisms for Hardware Veriﬁcation. In: VLSI Speciﬁcati- on, Veriﬁcation and Synthesis, Seiten 129–157, 1988. 326. M ERLIN , P. M.: A Study of the Recoverability of Computing Systems. Doktorarbeit, University of California, Irvine, Irvine, CA, U.S.A., 1974. ´ 327. M IN E , A.: The Octagon Abstract Domain. Higher Order and Symbolic Computation, 19(1):31–100, 2006. 328. http://www.model.com/. 329. M OLITOR , P. und J. M OHNKE: Equivalence Checking of Digital Circuits. Kluwer Aca- demic Publishers, Boston, 2004. ¨ 330. M OLLER , K.-H.: Ausgangsdaten f¨ r Qualit¨ tsmetriken – Eine Fundgrube f¨ r Analysen. u a u In: E BERT, C. und R. D UMKE (Herausgeber): Software-Metriken in der Praxis, Seiten 105 – 116. Springer, Berlin, 1996. 331. M OON , I.-H., J.H. K UKULA, K. R AVI und F. S OMENZI: To Split or to Conjoin: The Question in Image Computation. In: Proceedings of the Design Automation Conference (DAC), Seiten 23–28, 2000. 332. M OORE , G.: Cramming More Components onto Integrated Circuits. Electronics, 38:114–117, 1965. 333. M ORIN -A LLORY, K. und D. B ORRIONE: A Proof of Correctness for the Construction of Property Monitors. In: Proceedings of the High-Level Design Validation and Test Workshop (HLDVT), Seiten 237–244, 2005. 334. M ORIN -A LLORY, K. und D. B ORRIONE: On-Line Monitoring of Properties Built on Regular Expressions. In: Proceedings of the Forum on Design Languages (FDL), Seiten 249–254, 2006. 335. M ORIN -A LLORY, K. und D. B ORRIONE: Proven Correct Monitors from PSL Speciﬁ- cations. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 1246–1251, 2006. 336. M OSKEWICZ , M. W., C. F. M ADIGAN , Y. Z HAO, L. Z HANG und S. M ALIK: Chaff: Engineering an Efﬁcient SAT Solver. In: Proceedings of the Design Automation Confe- rence (DAC), Seiten 530–535, 2001. 337. M OY, M., F. M ARANINCHI und L. M AILLET-C ONTOZ: LusSy: A Toolbox for the Ana- lysis of Systems-on-a-Chip at the Transactional Level. In: Proceedings of the Internatio- nal Conference on Application of Concurrency to System Design (ACSD), Seiten 26–35, 2005. 338. M URATA , T.: Petri Nets: Properties, Analysis, and Applications. Proceedings of the IEEE, 77(4):541–580, 1989. 339. M USUVATHI , M., D. Y. W. PARK, A. C HOU, D. R. E NGLER und D. L. D ILL: CMC: A Pragmatic Approach to Model Checking Real Code. ACM SIGOPS Operating Systems Review, 36(SI):75–88, 2002. 340. NADEL , A LEXANDER: Backtrack Search Algorithms for Propositional Logic Satisﬁa- bility: Review and Innovations. Master Thesis, The Hebrew University of Jerusalem, Israel, 2002. 341. NAUR , P.: Checking of Operand Types in ALGOL Compilers. BIT Numerical Mathe- matics, 5(3):151–163, 1965. 342. N ELSON , C. G. und D. C. O PPEN: Simpliﬁcation by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245–257, 1979. 343. N IELSON , F., H. R. N IELSON und C. H ANKIN: Principles of Program Analysis. Sprin- ger, Heidelberg, Berlin, New York, 2005. 2. Auﬂage.
580 Literatur 344. N IEMANN , B. und C. H AUBELT: Assertion-Based Veriﬁcation of Transaction Level Mo- dels. In: Proceedings of Methoden und Beschreibungssprachen zur Modellierung und Veriﬁkation von Schaltungen und Systemen (MBMV), Seiten 232–236, 2006. 345. N IEMANN , B. und C. H AUBELT: Formalizing TLM with Communicating State Machi- nes. In: Proceedings of the Forum on Design Languages (FDL), Seiten 285–292, 2006. 346. N IEMANN , B. und C. H AUBELT: Towards a Uniﬁed Execution Model for Transactions in TLM. In: Proceedings of the International Conference on Formal Methods and Models for Co-Design (MEMOCODE), Seiten 103–112, 2007. 347. N IEMANN , B., C. H AUBELT, M. U RIBE und J. T EICH: Formalizing TLM with Com- municating State Machines. In: Advances in Design and Speciﬁcation Languages for Embedded Systems, Seiten 225–242. Springer, 2007. 348. N IEUWENHUIS , R. und A. O LIVERAS: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 321–334, 2005. 349. N TAFOS , S. C.: On Required Element Testing. IEEE Transactions on Software Engi- neering, SE-10(6):795–803, 1984. 350. N TAFOS , S. C.: A Comparison of some Structural Testing Strategies. IEEE Transactions on Software Engineering, 14(6):868–874, 1988. 351. http://www.accellera.org/. 352. OSCI TLM WORKING G ROUP: OSCI TLM-2.0 Language Reference Manual, 2009. Version JA32, http://www.systemc.org. 353. PARTHASARATHY, G., M. K. I YER, K.-T. C HENG und L.-C. WANG : An Efﬁcient Finite-Domain Constraint Solver for Circuits. In: Proceedings of the Design Automation Conference (DAC), Seiten 212–217, 2004. 354. PASRICHA , S., N. D UTT, E. B OZORGZADEH und M. B EN -ROMDHANE: FABSYN: Floorplan-aware Bus Architecture Synthesis. IEEE Transactions on Very Large Scale Integrated Systems, 14(3):241–253, 2006. 355. PATTERSON , D. A. und J. L. H ENNESSY: Computer Organization & Design: The Hardware/Software Interface. Morgan Kaufmann Publishers Inc., San Francisco, CA, U.S.A., 1997. 2. Auﬂage. 356. PCI S PECIAL I NTEREST G ROUP: PCI Local Bus Speciﬁcation, 1998. Version 2.2. 357. P ELED , D.: All from One, One for All: On Model Checking Using Representatives. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 409–423, 1993. 358. P ELED , D.: Combining Partial Order Reductions with On-the-Fly Model-Checking. Journal of Formal Methods in System Design, 8(1):39–64, 1996. 359. P ETERSON , J. L.: Petri Net Theory and Modeling of Systems. Prentice-Hall, Inc., Rea- ding, MA, 1981. 360. P ETRI , C. A.: Interpretations of a Net Theory. Technischer Bericht 75–07, GMD, Bonn, Germany, 1975. 361. P IERRE , L. und L. F ERRO: A Tractable and Fast Method for Monitoring SystemC TLM Speciﬁcations. IEEE Transactions on Computers, 57(10):1346–1356, 2008. 362. P ILARSKI , S. und G. H U: SAT with Partial Clauses and Back-Leaps. In: Proceedings of the Design Automation Conference (DAC), Seiten 743–746, 2002. 363. P IMENTEL , A. D., C. E RBAS und S. P OLSTRA: A Systematic Approach to Exploring Embedded System Architectures at Multiple Abstraction Levels. IEEE Transactions on Computers, 55(2):99–112, 2006. 364. P NUELI , A.: The Temporal Logic of Programs. In: Proceedings of the Symposium on Foundations of Computer Science, Seiten 46–57, 1977.
Literatur 581 365. P OP, T., P. E LES und Z. P ENG: Holistic Scheduling and Analysis of Mixed Time/Event- Triggered Distributed Embedded Systems. In: Proceedings of the Conference on Hard- ware/Software Codesign (CODES), Seiten 187–192, 2002. 366. P RASAD , M., A. B IERE und A. G UPTA : A Survey of Recent Advances in SAT-Based Formal Veriﬁcation. International Journal on Software Tools for Technology Transfer (STTT), 7(2):156–173, 2005. 367. P ROSSER , PATRICK: Hybrid Algorithms for the Constraint Satisfaction Problem. Com- putational Intelligence, 9(3):268–299, 1993. 368. P USCHNER , P. und C. K OZA: Calculating the Maximum, Execution Time of Real-Time Programs. Real-Time Systems, 1(2):159–176, 1989. 369. Q UEILLE , J.-P. und J. S IFAKIS: Speciﬁcation and Veriﬁcation of Concurrent Systems in CESAR. In: Proceedings of the Symposium on Programming, Seiten 337–351, 1982. 370. R AMCHANDANI , C.: Analysis of Asynchronous Concurrent Systems by Timed Petri Nets. Doktorarbeit, Massachusetts Institute of Technology, Cambridge, MA, U.S.A., 1974. 371. R AVI , K. und F. S OMENZI: High-Density Reachability Analysis. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 154–158, 1995. 372. R EDA , S. und A. S ALEM: Combinational Equivalence Checking Using Boolean Satis- ﬁability and Binary Decision Diagrams. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 122–126, 2001. 373. R EISIG , W.: A Primer in Petri Net Design. Springer, Berlin, Heidelberg, New York, Tokyo, 1992. 374. R EISIG , W.: Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer, Berlin, 1998. 375. R EITER , R.: Scheduling Parallel Computations. Journal of the ACM, 15(4):590–599, 1968. 376. R EYNOLDS , J. C.: Automatic Computation of Data Set Deﬁnitions. In: Proceedings of IFIP Congress, Band 1, Seiten 456–461, 1968. 377. R ICHTER , K.: Compositional Scheduling Analysis Using Standard Event Models. Dok- torarbeit, Technische Universit¨ t Braunschweig, Deutschland, 2004. a 378. R ICHTER , K. und R. E RNST: Event Model Interfaces for Heterogeneous System Ana- lysis. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 506–513, 2002. 379. R ICHTER , K., M. J ERSAK und R. E RNST: A Formal Approach to MPSoC Performance Veriﬁcation. IEEE Computer, 36(4):60–67, 2003. 380. R ICHTER , K., D. Z IEGENBEIN, M. J ERSAK und R. E RNST: Model Composition for Scheduling Analysis in Platform Design. In: Proceedings of the Design Automation Conference (DAC), Seiten 287–292, 2002. 381. ROTH , J. P.: Diagnosis of Automata Failures: A Calculus and a Method. IBM Journal of Research and Development, 10(4):278–291, 1966. 382. RTCA: Software Considerations in Airborne Systems and Equipment Certiﬁcation. DO- 178B, 1992. 383. RUDELL , R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Sei- ten 42–47, 1993. 384. http://www.haifa.ibm.com/projects/veriﬁcation/RB Homepage/. 385. S AFRA , S.: On the Complexity of ω -Automata. In: Proceedings of the Symposium on Foundations of Computer Science, Seiten 319–327, 1988.
582 Literatur ¨ 386. S CHIRNER , G. und R. D OMER: Quantitative Analysis of Transaction Level Models for the AMBA Bus. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 230–235, 2006. ¨ 387. S CHIRNER , G., A. G ERSTLAUER und R. D OMER: Abstract, Multifaceted Modeling of Embedded Processors for System Level Design. In: Proceedings of the Asia and South Paciﬁc Design Automation Conference (ASPDAC), Seiten 384–389, 2007. 388. S CHLIECKER , S., S. S TEIN und R. E RNST: Performance Analysis of Complex Systems by Integration of Dataﬂow Graphs and Compositional Performance Analysis. In: Pro- ceedings of the Design, Automation and Test in Europe (DATE), Seiten 273–278, 2007. 389. S CHMIDT, D. A.: Data Flow Analysis is Model Checking of Abstract Interpretations. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), Seiten 38–48, 1998. 390. S CHNEIDER , K.: Veriﬁcation of Reactive Systems – Formal Methods and Algorithms. Springer, Berlin, Heidelberg, 2004. 391. S CHNERR , J., O. B RINGMANN, A. V IEHL und W. ROSENSTIEL: High-Performance Timing Simulation of Embedded Software. In: Proceedings of the Design Automation Conference (DAC), Seiten 290–295, 2008. 392. S EBASTIANI , ROBERTO: Lazy Satisﬁability Modulo Theories. Journal on Satisﬁability, Boolean Modeling and Computation, 3:141–224, 2007. 393. S HANNON , C. E.: The Synthesis of Two-Terminal Switching Circuits. Bell Systems Technical Journal, 28:59–98, 1949. 394. S HASHIDHAR , K. C., M. B RUYNOOGHE , F. C ATTHOOR und G. JANSSENS: Automatic Functional Veriﬁcation of Memory Oriented Global Source Code Transformations. In: Proceedings of the High-Level Design Validation and Test Workshop (HLDVT), Seiten 31–36, 2003. 395. S HASHIDHAR , K. C., M. B RUYNOOGHE, F. C ATTHOOR und G. JANSSENS: Func- tional Equivalence Checking for Veriﬁcation of Algebraic Transformations on Array- Intensive Source Code. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 1310–1315, 2005. 396. S HASHIDHAR , K. C., M. B RUYNOOGHE, F. C ATTHOOR und G. JANSSENS: Veriﬁca- tion of Source Code Transformations by Program Equivalence Checking . In: Compiler Construction, Seiten 221–236. Springer, 2005. 397. S HEINI , H. M. und K. A. S AKALLAH: A Scalable Method for Solving Satisﬁability of Integer Linear Arithmetic Logic. In: Theory and Applications of Satisﬁability Testing, Seiten 241–256, 2005. 398. S HEKHAR , N., P. K ALLA und F. E NESCU : Equivalence Veriﬁcation of Polynomial Da- tapaths Using Ideal Membership Testing. IEEE Transactions on Computer-Aided De- sign of Integrated Circuits and Systems, 26(7):1320–1330, 2007. 399. S HOSTAK , R. E.: A Practical Decision Procedure for Arithmetic with Function Sym- bols. Journal of the ACM, 26(2):351–360, 1979. 400. S HOSTAK , R. E.: Deciding Combinations of Theories. Journal of the ACM, 31(1):1–12, 1984. 401. S HTRICHMAN , O.: Pruning Techniques for the SAT-Based Bounded Model Checking Problem. In: Proceedings of Conference on Correct Hardware Design and Veriﬁcation Methods (CHARME), Seiten 58–70, 2001. 402. S IEBENBORN , A., A. V IEHL, O. B RINGMANN und W. ROSENSTIEL: Control-Flow Aware Communication and Conﬂict Analysis of Parallel Processes. In: Proceedings of the Asia and South Paciﬁc Design Automation Conference (ASPDAC), Seiten 32–37, 2007.
Literatur 583 403. S KAKKEBÆK , J. U., R. B. J ONES und D. L. D ILL: Formal Veriﬁcation of Out-of-Order Execution Using Incremental Flushing. In: Proceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 98–109, 1998. 404. http://www.averant.com/products-solidify.html. 405. S OMENZI , F. und R. B LOEM: Efﬁcient B¨ chi Automata from LTL Formulae. In: Pro- u ceedings of the International Conference on Computer Aided Veriﬁcation (CAV), Seiten 248–263, 2000. 406. S PURI , M.: Earliest Deadline Scheduled in Real-Time Systems. Doktorarbeit, INRIA, Le Chesnay, Cedex, France, 1995. 407. S PURI , M.: Analysis of Deadline Scheduled Real-Time Tasks. Technischer Bericht, IN- RIA, Le Chesnay, Cedex, France, 1996. 408. S TANKOVIC , J., M. S PURI, K. R AMAMRITHAM und G. B UTTAZZO : Deadline Schedu- ling for Real-Time Systems – EDF and Related Algorithms. Kluwer Academic Publis- hers, Boston, MA, U.S.A., 1998. 409. S TARKE , P. H.: Analyse von Petri-Netz-Modellen. Teubner, Stuttgart, 1990. 410. S TEFFEN , B.: Data Flow Analysis as Model Checking. In: ’Proceedings of the In- ternational Conference on Theoretical Aspects of Computer Software (TACS), Seiten 346–365, 1991. 411. S TOFFEL , D. und W. K UNZ: Record & Play: A Structural Fixed Point Iteration for Sequential Circuit Veriﬁcation. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 394–399, 1997. 412. S TOFFEL , D., M. W EDLER, P. WARKENTIN und W. K UNZ: Structural FSM traver- sal. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 23(5):598–619, 2004. 413. S TRAHM , T.: Logik in Informatik, Mathematik und Philosophie, 1999. Vortrag anl¨ ss- a lich der Veranstaltung Theodor-Kocher-Preis 1998 der Universit¨ t Bern. a 414. S TREHL , K.: Symbolic Methods Applied to Formal Veriﬁcation and Synthesis in Em- bedded Systems Design. Doktorarbeit, Swiss Federal Institute of Technology Zurich, Switzerland, 2000. 415. S TREHL , K. und L. T HIELE: Symbolic Model Checking of Process Networks Using Interval Diagram Techniques. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 686–692, 1998. 416. S TREHL , K. und L. T HIELE: Interval Diagram Techniques for Symbolic Model Checking of Petri Nets. In: Proceedings of the Design, Automation and Test in Euro- pe (DATE), Seiten 756–757, 1999. 417. S TREHL , K., L. T HIELE, M. G RIES, D. Z IEGENBEIN, R. E RNST und J. T EICH: Fun- State – An Internal Design Representation for Codesign. IEEE Transactions on Very Large Scale Integrated Systems, 9(4):524–544, 2001. 418. S TREHL , K., L. T HIELE , D. Z IEGENBEIN, R. E RNST und J. T EICH: Scheduling Hard- ware/Software Systems Using Symbolic Techniques. In: Proceedings of the Conference on Hardware/Software Codesign (CODES), Seiten 173–177, 1999. ¨ 419. S TREUB UHR , M., J. FALK, C. H AUBELT, J. T EICH , R. D ORSCH und T. S CHLIPF: Task-Accurate Performance Modeling in SystemC for Real-Time Multi-Processor Archi- tectures. In: Proceedings of the Design, Automation and Test in Europe (DATE), Seiten 480–481, 2006. ¨ 420. S TREUB UHR , M., J. G LADIGAU, C. H AUBELT und J. T EICH: Efﬁcient Approximately- Timed Performance Modeling for Architectural Exploration of MPSoCs. In: Proceedings of the Forum on Design Languages (FDL), 2009. 421. S TROUSTRUP, B.: The C++ Programming Language: Language Library and Design Tutorial. Addison-Wesley, Amsterdam, 1997.