• aiT (2000) aiT WCET analyzer.http://www.absint.com/ait

• Altmeyer S, Burguière C (2009) A new notion of useful cache block to improve the bounds of cache-related preemption delay. In: ECRTS, pp 109–118

  Google Scholar 

• Altmeyer S, Maiza C, Reineke J (2010) Resilience analysis: tightening the CRPD bound for set-associative caches. In: LCTES, pp 153–162

  Google Scholar 

• Balakrishnan G, Reps TW (2004) Analyzing memory accesses in x86 executables. In: CC, pp 5–23

  Google Scholar 

• Balakrishnan G, Reps TW, Kidd N, Lal A, Lim J, Melski D, Gruian R, Yong SH, Chen CH, Teitelbaum T (2005) Model checking x86 executables with codesurfer/x86 and wpds++. In: CAV, pp 158–163

  Google Scholar 

• Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp 209–224

  Google Scholar 

• Chattopadhyay S, Roychoudhury A (2011) Scalable and precise refinement of cache timing analysis via model checking. In: RTSS, pp 193–203

  Google Scholar 

• Chattopadhyay S, Roychoudhury A, Mitra T (2010) Modeling shared cache and bus in multi-cores for timing analysis. In: SCOPES, pp 6–15

  Google Scholar 

• Chattopadhyay S, Chong LK, Roychoudhury A, Kelter T, Marwedel P, Falk H (2012) A unified WCET analysis framework for multi-core platforms. In: RTAS, pp 99–108

  Google Scholar 

• Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, pp 168–176

  Google Scholar 

• Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263

  Article MATH  Google Scholar 

• Clarke EM, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Methods Syst Des 19(1):7–34

  Article MATH  Google Scholar 

• Dalsgaard AE, Olesen MC, Toft M, Hansen RR, Larsen KG (2010) METAMOC: modular execution time analysis using model checking. In: WCET, pp 113–123

  Google Scholar 

• Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In: PLDI, pp 213–223

  Google Scholar 

• Grund D, Reineke J (2010a) Precise and efficient FIFO-replacement analysis based on static phase detection. In: ECRTS, pp 155–164

  Google Scholar 

• Grund D, Reineke J (2010b) Toward precise PLRU cache analysis. In: WCET, pp 23–35

  Google Scholar 

• Gustafsson J, Betts A, Ermedahl A, Lisper B (2010) The Mälardalen WCET benchmarks—past present and future. In: WCET, pp 137–147.http://www.mrtc.mdh.se/projects/wcet/benchmarks.html

  Google Scholar 

• Hardy D, Piquet T, Puaut I (2009) Using bypass to tighten WCET estimates for multi-core processors with shared instruction caches. In: RTSS, pp 68–77

  Google Scholar 

• Huber B, Schoeberl M (2009) Comparison of implicit path enumeration and model checking based WCET analysis. In: WCET

  Google Scholar 

• Huynh BK, Ju L, Roychoudhury A (2011) Scope-aware data cache analysis for WCET estimation. In: RTAS, pp 203–212

  Google Scholar 

• Ju L, Huynh BK, Roychoudhury A, Chakraborty S (2008) Performance debugging of esterel specifications. In: CODES+ISSS, pp 173–178

  Google Scholar 

• Kelter T, Falk H, Marwedel P, Chattopadhyay S, Roychoudhury A (2011) Bus-aware multicore WCET analysis through TDMA offset bounds. In: ECRTS, pp 3–12

  Google Scholar 

• King JC (1976) Symbolic execution and program testing. Commun ACM 19(7):385–394

  Article MATH  Google Scholar 

• KLEE (2008) The KLEE symbolic virtual machine.http://klee.llvm.org

• Lee CG, Hahn J, Seo YM, Min SL, Ha R, Hong S, Park CY, Lee M, Kim CS (1998) Analysis of cache-related preemption delay in fixed-priority preemptive scheduling. IEEE Trans Comput 47(6):700–713

  Article MathSciNet  Google Scholar 

• Li X, Roychoudhury A, Mitra T (2004) Modeling out-of-order processors for software timing analysis. In: RTSS, pp 92–103

  Google Scholar 

• Li X, Liang Y, Mitra T, Roychoudhury A (2007) Chronos: a timing analyzer for embedded software. In: Science of computer programming, pp 56–67.http://www.comp.nus.edu.sg/~rpembed/chronos

  Google Scholar 

• Li Y, Suhendra V, Liang Y, Mitra T, Roychoudhury A (2009) Timing analysis of concurrent programs running on shared cache multi-cores. In: RTSS, pp 57–67

  Google Scholar 

• Li YTS, Malik S, Wolfe A (1999) Performance estimation of embedded software with instruction cache modeling. ACM Trans Des Autom Electron Syst 4(3):257–279

  Article  Google Scholar 

• LLVM (2003) The LLVM compiler infrastructure.http://llvm.org

• Lv M, Yi W, Guan N, Yu G (2010) Combining abstract interpretation with model checking for timing analysis of multicore software. In: RTSS, pp 339–349

  Google Scholar 

• Metzner A (2004) Why model checking can improve WCET analysis. In: CAV, pp 334–347

  Google Scholar 

• Negi HS, Mitra T, Roychoudhury A (2003) Accurate estimation of cache-related preemption delay. In: CODES+ISSS, pp 201–206

  Google Scholar 

• Pellizzoni R, Schranzhofer A, Chen JJ, Caccamo M, Thiele L (2010) Worst case delay analysis for memory interference in multicore systems. In: DATE, pp 741–746

  Google Scholar 

• Reineke J, Grund D (2008) Relative competitive analysis of cache replacement policies. In: LCTES, pp 51–60

  Chapter  Google Scholar 

• Reineke J, Grund D, Berg C, Wilhelm R (2007) Timing predictability of cache replacement policies. Real-Time Syst 37(2):99–122

  Article MATH  Google Scholar 

• SPIN (1991) SPIN model checker.http://spinroot.com/spin/whatispin.html

• STP (2007) The STP constraint solver.http://sites.google.com/site/stpfastprover

• Suhendra V, Mitra T, Roychoudhury A, Chen T (2006) Efficient detection and exploitation of infeasible paths for software timing analysis. In: DAC, pp 358–363

  Google Scholar 

• Tan Y, Mooney V (2007) Timing analysis for preemptive multitasking real-time systems with caches. ACM Trans Embed Comput Syst 6(1)

• Theiling H, Ferdinand C, Wilhelm R (2000) Fast and precise WCET prediction by separated cache and path analyses. Real-Time Syst 18(2/3):157–179

  Article  Google Scholar 

• Wilhelm R (2004) Why AI + ILP is good for WCET, but MC is not, nor ILP alone. In: VMCAI, pp. 309–322

  Google Scholar 

• Wilhelm R, Grund D, Reineke J, Schlickling M, Pister M, Ferdinand C (2009) Memory hierarchies, pipelines, and buses for future architectures in time-critical embedded systems. IEEE Trans Comput-Aided Des Integr Circuits Syst 28(7):966–978

  Article  Google Scholar 

• Yan J, Zhang W (2008) WCET analysis for multi-core processors with shared L2 instruction caches. In: RTAS, pp 80–89

  Google Scholar 

Download references