M. F. Atig, A. Bouajjani, S. Burckhardt & M. Musuvathi (2010):
On the verification problem for weak memory models.
In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages,
POPL '10.
ACM,
New York, NY, USA,
pp. 7–18,
doi:10.1145/1706299.1706303.
Atmel Corporation (2009):
The Atmel 8-bit AVR Microcontroller with 16K Bytes of In-system Programmable Flash.
www.atmel.com/atmel/acrobat/doc2466.pdf.
E. Beckschulze, J. Brauer & S. Kowalewski (2012):
Access-Based Localization for Octagons.
Electronic Notes in Theoretical Computer Science 287(0),
pp. 29 – 40,
doi:10.1016/j.entcs.2012.09.004.
Proceedings of the Fourth International Workshop on Numerical and Symbolic Abstract Domains, (NSAD 2012).
E. Beckschulze, J. Brauer, A. Stollenwerk & S. Kowalewski (2011):
Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations.
In: 14th IEEE Int. Symp. on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops.
IEEE,
pp. 33–40,
doi:10.1109/ISORCW.2011.40.
H.-J. Boehm & S. V. Adve (2008):
Foundations of the C++ concurrency memory model.
In: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation,
PLDI '08.
ACM,
New York, NY, USA,
pp. 68–78,
doi:10.1145/1375581.1375591.
N. Cooprider (2008):
Data-flow analysis for interrupt-driven microcontroller software.
The University of Utah,
Salt Lake City, UT, USA.
P. Cousot & R. Cousot (1977):
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.
In: POPL.
ACM Press,
pp. 238–252,
doi:10.1145/512950.512973.
A. Fehnker, R. Huuck, B. Schlich & M. Tapp (2009):
Automatic Bug Detection in Microcontroller Software by Static Program Analysis.
In: SOFSEM 2009: Theory and Practise of Computer Science,Spindleruv Mlýn, Czech Republic,
Lecture Notes in Computer Science 5404.
Springer,
pp. 267–278,
doi:10.1007/978-3-540-95891-8_26.
P. Godefroid (1996):
Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem.
LNCS 1032.
Springer,
doi:10.1007/3-540-60761-7.
T. E. Hart, P. E. McKenney & A. D. Brown (2006):
Making Lockless Synchronization Fast: Performance Implications of Memory Reclamation.
In: 20th IEEE International Parallel and Distributed Processing Symposium,
Rhodes, Greece,
doi:10.1109/IPDPS.2006.1639261.
ISO (1999):
ANSI/ISO/IEC 9899-1999: Programming Languages — C.
International Organization for Standardization,
Geneva, Switzerland.
S. Meyers & A. Alexandrescu (2004):
C++ and the perils of double-checked locking.
http://www.aristeia.com/Papers/DDJ_Jul_Aug_2004_revised.pdf.
A. Miné (2006):
The Octagon Abstract Domain.
Higher-Order and Symbolic Computation 19(1),
pp. 31–100,
doi:10.1007/s10990-006-8609-1.
A. Miné (2012):
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs.
Logical Methods in Computer Science 8(1–26),
pp. 1–63.
H. Oh, L. Brutschy & K. Yi (2011):
Access analysis-based tight localization of abstract memories.
In: Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation,
VMCAI'11.
Springer-Verlag,
Berlin, Heidelberg,
pp. 356–370,
doi:10.1007/978-3-642-18275-4_25.
P. Pratikakis, J. S. Foster & M. Hicks (2011):
LOCKSMITH: Practical static race detection for C.
ACM Trans. Program. Lang. Syst. 33(1),
pp. 3:1–3:55,
doi:10.1145/1889997.1890000.
J. Regehr & N. Cooprider (2007):
Interrupt Verification via Thread Verification.
Electron. Notes Theor. Comput. Sci. 174(9),
pp. 139–150,
doi:10.1016/j.entcs.2007.04.002.
B. Schlich, T. Noll, J. Brauer & L. Brutschy (2009):
Reduction of Interrupt Handler Executions for Model Checking Embedded Software.
In: Haifa Verification Conference (HVC 2009), Haifa, Israel,
LNCS 6405.
Springer,
pp. 5–20,
doi:10.1007/978-3-642-19237-1_5.
eptcs@eptcs.org