Achim D. Brucker - Publications (by Topic)

Information Security

Achim Brucker is interested a wide range of security topics in general and security engineering in particular. This includes the use of formal methods for, e.g., analyzing security architectures [brucker.ea:verification:2005, brucker.ea:case:2003], modeling of security policies [brucker.ea:model-based:2011], security conformance testing of systems [brucker.ea:test-sequence:2007, brucker.ea:model-based:2011, brucker.ea:firewall:2010], and protocol verification [brucker.ea:integrating:2009]. More applied, he works on model-driven security [brucker.ea:mda:2006-b] approaches such as SecureUML (based on UML/OCL) [brucker.ea:transformation:2006, brucker.ea:extending:2009] and SecureBPMN (based on BPMN) [brucker:securebpmn:2013, brucker.ea:securebpmn:2012, brucker.ea:framework:2013, compagna.ea:bp-compliance:2013]. The latter includes also a various other business-process security topics, e.g., [brucker.ea:secure:2012, brucker.ea:securebpmn:2012, monakova.ea:securing:2012, monakova.ea:monitoring:2012, kohler.ea:proactive:2009, brucker.ea:modellierung:2010, kohler.ea:caching:2010]. Moreover, he works security for services (i.e., cloud-based and service-oriented systems), e.g., [marienfeld.ea:usdl-security:2012, brucker.ea:secure:2012, brucker.ea:framework:2011] and on various aspects of access control policies including performance improvements of access control enforcement infrastructures [kohler.ea:proactive:2009, kohler.ea:caching:2010, brucker.ea:efficient:2010], management of access control infrastructures (e.g. using XACML) [brucker.ea:framework:2011], as well as access control for exceptional situations, called break-(the)-glass access control [brucker.ea:attribute-based:2010, brucker.ea:extending:2009] or access control for disaster management systems [brucker.ea:information:2010].

[-] Publications
(Click To Expand)

[77]

A. D. Brucker and S. Yalman, “Ensuring confidentiality in supply chains with an application to life-cycle assessment,” Software: Practice and Experience (SPE), 2025, doi: 10.1002/smr.2763. Author copy: https://logicalhacking.com/publications/brucker.ea-confidential-supply-chains-2025/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[76]

D. Marmsoler, A. Ahmed, and A. D. Brucker, “Secure smart contracts with Isabelle/Solidity,” in Software engineering and formal methods (SEFM), A. Madeira and A. Knapp, Eds. Heidelberg: Springer-Verlag, 2024. doi: 10.1007/978-3-031-77382-2_10. Author copy: https://logicalhacking.com/publications/marmsoler.ea-secure-smart-contracts-2024/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[75]

A. D. Brucker and D. Marmsoler, “Teaching formal methods in application domains: A case study in computer and network security,” in Formal methods teaching (FMTea 2024), L. Ribeiro and E. Sekerinski, Eds. Heidelberg: Springer-Verlag, 2024. doi: 10.1007/978-3-031-71379-8_8. Author copy: https://logicalhacking.com/publications/brucker.ea-fm-teaching-2024/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[74]

A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition in Isabelle/HOL,” ACM Transactions on Privacy and Security, 2023, doi: 10.1145/3577020. Author copy: https://logicalhacking.com/publications/hess.ea-stateful-protocol-composition-2023/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[73]

[72]

A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “Performing security proofs of stateful protocols,” in 34th IEEE computer security foundations symposium (CSF), 2021, vol. 1, pp. 143–158. doi: 10.1109/CSF51468.2021.00006. Author copy: https://logicalhacking.com/publications/hess.ea-performing-2021/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[71]

A. D. Brucker and M. Herzberg, “A formalization of safely composable web components,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/SC_DOM_Components.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-sc-dom-components-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[70]

A. D. Brucker and M. Herzberg, “A formalization of web components,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/DOM_Components.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-dom-components-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[69]

A. D. Brucker and M. Herzberg, “Shadow SC DOM: A formal model of the safelty composable document object model with shadow roots,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Shadow_SC_DOM.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-shadow-sc-dom-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[68]

A. D. Brucker and M. Herzberg, “Shadow DOM: A formal model of the document object model with shadow roots,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Shadow_DOM.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-shadow-dom-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[67]

A. D. Brucker and M. Herzberg, “The safely composable DOM,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Core_SC_DOM.html, Formal proof development
[Abstract | BibTeX | RIS | EndNote | Word]

[66]

A. V. Hess, S. Mödersheim, A. D. Brucker, and A. Schlichtkrull, “Automated stateful protocol verification,” Archive of Formal Proofs, Apr. 2020. https://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html, Formal proof development. Author copy: https://logicalhacking.com/publications/hess.ea-automated-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[65]

A. V. Hess, S. Mödersheim, and A. D. Brucker, “Stateful protocol composition and typing,” Archive of Formal Proofs, Apr. 2020. https://www.isa-afp.org/entries/Stateful_Protocol_Composition_and_Typing.html, Formal proof development. Author copy: https://logicalhacking.com/publications/hess.ea-stateful-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[64]

S. Dashevskyi, A. D. Brucker, and F. Massacci, “A screening test for disclosed vulnerabilities in FOSS components,” IEEE Trans. Software Eng., vol. 45, no. 10, pp. 945–966, Oct. 2019, doi: 10.1109/TSE.2018.2816033. Author copy: https://logicalhacking.com/publications/dashevskyi.ea-vulnerability-screening-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[63]

A. D. Brucker and M. Herzberg, “The Core DOM,” Archive of Formal Proofs, Dec. 2018. https://www.isa-afp.org/entries/Core_DOM.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-core-dom-2018/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[62]

A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition,” in ESORICS, J. Lopez and J. Zhou, Eds. Heidelberg: Springer-Verlag, 2018, pp. 427–446. doi: 10.1007/978-3-319-99073-6. Author copy: https://logicalhacking.com/publications/hess.ea-stateful-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[61]

A. V. Hess, S. A. Mödersheim, and A. D. Brucker, “Stateful protocol composition (extended version),” DTU Compute, Technical University Denmark, 2018-03, 2018. Author copy: https://logicalhacking.com/publications/hess.ea-tr-stateful-protocol-2018/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[60]

[59]

M. Asim, A. Yautsiukhin, A. D. Brucker, T. Baker, Q. Shi, and B. Lempereur, “Security policy monitoring of BPMN-based service compositions,” Journal of Software: Evolution and Process, 2018, doi: 10.1002/smr.1944. Author copy: https://logicalhacking.com/publications/asim.ea-policy-monitoring-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[58]

A. D. Brucker and M. Herzberg, “A formal semantics of the Core DOM in Isabelle/HOL,” in The 2018 web conference companion (WWW), 2018, pp. 741–749. doi: 10.1145/3184558.3185980. Author copy: https://logicalhacking.com/publications/brucker.ea-core-dom-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[57]

A. D. Brucker, “Theorem prover-based testing: Combining verification and testing,” presented at the Midlands graduate school, Leicester, UK, Apr. 09, 2017.
[Abstract | BibTeX | RIS | EndNote | Word]

[56]

A. D. Brucker, B. Zhou, F. Malmignati, Q. Shi, and M. Merabti, “Modelling, validating, and ranking of secure service compositions,” Software: Practice and Expierence (SPE), vol. 47, pp. 1912–1943, Dec. 2017, doi: 10.1002/spe.2513. Author copy: https://logicalhacking.com/publications/brucker.ea-secure-services-2017/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[55]

L. ben Othmane, A. D. Brucker, S. Dashevskyi, and P. Tsalovski, “An introduction to data analytics for software security,” in Empirical research for software security: Foundations and experience, L. ben Othmane, M. G. Jaatun, and E. Weippl, Eds. CRC Press, 2017, pp. 69–94. Author copy: https://logicalhacking.com/publications/othmane.ea-data-analytics-2017/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[54]

L. ben Othmane, G. Chehrazi, E. Bodden, P. Tsalovski, and A. D. Brucker, “Time for addressing software security issues: Prediction models and impacting factors,” Data Science and Engineering (DSEJ), vol. 2, no. 2, pp. 107–124, 2017, doi: 10.1007/s41019-016-0019-8. Author copy: https://logicalhacking.com/publications/othmane.ea-fix-effort-2016/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[53]

A. D. Brucker, L. Brügger, and B. Wolff, “Formal network models and their application to firewall policies,” Archive of Formal Proofs, Jan. 2017. https://www.isa-afp.org/entries/UPF_Firewall.shtml, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-upf-firewall-2017/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[52]

A. D. Brucker, “Sicherheitstests für secure DevOps (SecDevOps),” OBJEKTspektrum, May 2016, https://www.sigs-datacom.de/uploads/tx_dmjournals/brucker_OTS_DevOps_16.pdf Online Themenspecial DevOps 2016.
[Abstract | BibTeX | RIS | EndNote | Word]

[51]

S. Dashevskyi, A. D. Brucker, and F. Massacci, “On the security cost of using a free and open source component in a proprietary product,” in International symposium on engineering secure software and systems (ESSoS), J. Caballero and E. Bodden, Eds. Heidelberg: Springer-Verlag, 2016, pp. 190–206. doi: 10.1007/978-3-319-30806-7_12. Author copy: https://logicalhacking.com/publications/dashevskyi.ea-foss-costs-2016/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[50]

A. D. Brucker and M. Herzberg, “On the static analysis of hybrid mobile apps: A report on the state of apache cordova nation,” in International symposium on engineering secure software and systems (ESSoS), J. Caballero and E. Bodden, Eds. Heidelberg: Springer-Verlag, 2016, pp. 72–88. doi: 10.1007/978-3-319-30806-7_5. Author copy: https://logicalhacking.com/publications/brucker.ea-cordova-security-2016/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[49]

M. Felderer, M. Büchler, M. Johns, A. D. Brucker, R. Breu, and A. Pretschner, “Security testing: A survey,” Advances in Computers, vol. 101, pp. 1–51, Mar. 2016, doi: 10.1016/bs.adcom.2015.11.003. Author copy: https://logicalhacking.com/publications/felderer.ea-security-testing-2016/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[48]

L. ben Othmane, G. Chehrazi, E. Bodden, P. Tsalovski, and A. D. Brucker, “Time for addressing software security issues: Prediction models and impacting factors,” Technische Universität Darmstadt, TUD-CS-2015-1268, Nov. 2015. Author copy: https://logicalhacking.com/publications/othmane.ea-time-2015/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[47]

L. ben Othmane, G. Chehrazi, E. Bodden, P. Tsalovski, A. D. Brucker, and P. Miseldine, “Factors impacting the effort required to fix security vulnerabilities: An industrial case study,” in Information security conference (ISC 2015), C. Boyd and D. Gligoriski, Eds. Heidelberg: Springer-Verlag, 2015. doi: 10.1007/978-3-319-23318-5_6. Author copy: https://logicalhacking.com/publications/othmane.ea-fix-effort-2015/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[46]

M. Salnitri, A. D. Brucker, and P. Giorgini, “From secure business process models to secure artifact-centric specifications,” in Enterprise, business-process and information systems modeling BPMDS, 2015, pp. 246–262. doi: 10.1007/978-3-319-19237-6_16. Author copy: https://logicalhacking.com/publications/salnitri.ea-river-2015/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[45]

A. D. Brucker, L. Brügger, and B. Wolff, “Formal firewall conformance testing: An application of test and proof techniques,” Software Testing, Verification & Reliability (STVR), vol. 25, no. 1, pp. 34–71, 2015, doi: 10.1002/stvr.1544. Author copy: https://logicalhacking.com/publications/brucker.ea-formal-fw-testing-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[44]

A. D. Brucker, L. Brügger, and B. Wolff, “The unified policy framework (UPF),” Archive of Formal Proofs, Nov. 2014. https://www.isa-afp.org/entries/UPF.shtml, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-upf-2014/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[43]

[42]

M. Asim, A. Yautsiukhin, A. D. Brucker, B. Lempereur, and Q. Shi, “Security policy monitoring of composite services,” in Secure and trustworthy service composition: The aniketos approach, A. D. Brucker, F. Dalpiaz, P. Giorgini, P. H. Meland, and E. Rios, Eds. Heidelberg: Springer-Verlag, 2014, pp. 192–202. doi: 10.1007/978-3-319-13518-2_13. Author copy: https://logicalhacking.com/publications/asim.ea-aniketos-monitoring-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[41]

A. D. Brucker, L. Compagna, and P. Guilleminot, “Compliance validation of secure service compositions,” in Secure and trustworthy service composition: The aniketos approach, A. D. Brucker, F. Dalpiaz, P. Giorgini, P. H. Meland, and E. Rios, Eds. Heidelberg: Springer-Verlag, 2014, pp. 136–149. doi: 10.1007/978-3-319-13518-2_10. Author copy: https://logicalhacking.com/publications/brucker.ea-aniketos-compliance-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[40]

A. D. Brucker, F. Malmignati, M. Merabti, Q. Shi, and B. Zhou, “Aniketos service composition framework: Analysing and ranking of secure services,” in Secure and trustworthy service composition: The aniketos approach, A. D. Brucker, F. Dalpiaz, P. Giorgini, P. H. Meland, and E. Rios, Eds. Heidelberg: Springer-Verlag, 2014, pp. 121–135. doi: 10.1007/978-3-319-13518-2_9. Author copy: https://logicalhacking.com/publications/brucker.ea-aniketos-scf-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[39]

A. D. Brucker, “Using SecureBPMN for modelling security-aware service compositions,” in Secure and trustworthy service composition: The aniketos approach, A. D. Brucker, F. Dalpiaz, P. Giorgini, P. H. Meland, and E. Rios, Eds. Heidelberg: Springer-Verlag, 2014, pp. 110–120. doi: 10.1007/978-3-319-13518-2_8. Author copy: https://logicalhacking.com/publications/brucker-aniketos-securebpmn-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[38]

P. H. Meland, E. Rios, V. Tountopoulos, and A. D. Brucker, “The aniketos platform,” in Secure and trustworthy service composition: The aniketos approach, A. D. Brucker, F. Dalpiaz, P. Giorgini, P. H. Meland, and E. Rios, Eds. Heidelberg: Springer-Verlag, 2014. doi: 10.1007/978-3-319-13518-2_4. Author copy: https://logicalhacking.com/publications/meland.ea-aniketos-platform-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[37]

R. Bachmann and A. D. Brucker, “Developing secure software: A holistic approach to security testing,” Datenschutz und Datensicherheit (DuD), vol. 38, no. 4, pp. 257–261, Apr. 2014, doi: 10.1007/s11623-014-0102-0. Author copy: https://logicalhacking.com/publications/bachmann.ea-security-testing-2014/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[36]

[35]

A. D. Brucker and U. Sodan, “Deploying static application security testing on a large scale,” in GI sicherheit 2014, Mar. 2014, vol. 228, pp. 91–101. Author copy: https://logicalhacking.com/publications/brucker.ea-sast-expierences-2014/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[34]

A. D. Brucker, “Model-based testing for secure services,” presented at the Aniketos spring ph.d. School on “trustworthy & secure service composition,” Malaga, Spain, May 30, 2013.
[Abstract | BibTeX | RIS | EndNote | Word]

[33]

A. D. Brucker, “Integrating security aspects into business process models,” it - Information Technology, vol. 55, no. 6, pp. 239–246, Dec. 2013, doi: 10.1524/itit.2013.2004. Special Issue on “Security in Business Processes.” Author copy: https://logicalhacking.com/publications/brucker-securebpmn-2013/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[32]

A. D. Brucker, F. Malmignati, M. Merabti, Q. Shi, and B. Zhou, “A framework for secure service composition,” in International conference on information privacy, security, risk and trust (PASSAT), Los Alamitos, CA, USA: IEEE Computer Society, 2013, pp. 647–652. doi: 10.1109/SocialCom.2013.97. Author copy: https://logicalhacking.com/publications/brucker.ea-framework-2013/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[31]

A. D. Brucker, L. Brügger, and B. Wolff, “HOL-TestGen/FW: An environment for specification-based firewall conformance testing,” in International colloquium on theoretical aspects of computing (ICTAC), Z. Liu, J. Woodcock, and H. Zhu, Eds. Heidelberg: Springer-Verlag, 2013, pp. 112–121. doi: 10.1007/978-3-642-39718-9_7. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-testgen-fw-2013/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[30]

L. Compagna, P. Guilleminot, and A. D. Brucker, “Business process compliance via security validation as a service,” in IEEE sixth international conference on software testing, verification and validation (ICST), 2013, pp. 455–462. doi: 10.1109/ICST.2013.63. Author copy: https://logicalhacking.com/publications/compagna.ea-bp-compliance-2013/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[29]

A. D. Brucker and I. Hang, “Secure and compliant implementation of business process-driven systems,” in Joint workshop on security in business processes (SBP), 2012, vol. 132, pp. 662–674. doi: 10.1007/978-3-642-36285-9_66. Author copy: https://logicalhacking.com/publications/brucker.ea-secure-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[28]

G. Monakova, C. Severin, A. D. Brucker, U. Flegel, and A. Schaad, “Monitoring security and safety of assets in supply chains,” in Future security, 2012, vol. 318, pp. 9–20. doi: 10.1007/978-3-642-33161-9_3. Author copy: https://logicalhacking.com/publications/monakova.ea-monitoring-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[27]

A. D. Brucker, I. Hang, G. Lückemeyer, and R. Ruparel, “SecureBPMN: Modeling and enforcing access control requirements in business processes,” in ACM symposium on access control models and technologies (SACMAT), 2012, pp. 123–126. doi: 10.1145/2295136.2295160. Author copy: https://logicalhacking.com/publications/brucker.ea-securebpmn-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[26]

G. Monakova, A. D. Brucker, and A. Schaad, “Security and safety of assets in business processes,” in ACM symposium on applied computing (SAC), 2012, pp. 1667–1673. doi: 10.1145/2245276.2232045. Author copy: https://logicalhacking.com/publications/monakova.ea-securing-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[25]

F. Marienfeld et al., “Service levels, security, and trust,” in Handbook of service description: USDL and its methods, A. Barros and D. Oberle, Eds. New York, NY, USA: Springer-Verlag, 2012, pp. 295–326. doi: 10.1007/978-1-4614-1864-1_12. Author copy: https://logicalhacking.com/publications/marienfeld.ea-usdl-security-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[24]

A. D. Brucker, L. Brügger, P. Kearney, and B. Wolff, “An approach to modular and testable security models of real-world health-care applications,” in ACM symposium on access control models and technologies (SACMAT), 2011, pp. 133–142. doi: 10.1145/1998441.1998461. Author copy: https://logicalhacking.com/publications/brucker.ea-model-based-2011/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[23]

A. D. Brucker and H. Petritsch, “A framework for managing and analyzing changes of security policies,” in IEEE international symposium on policies for distributed systems and networks (POLICY), Jun. 2011, pp. 105–112. doi: 10.1109/POLICY.2011.47. Author copy: https://logicalhacking.com/publications/brucker.ea-framework-2011/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[22]

M. Kohler and A. D. Brucker, “Caching strategies: An empirical evaluation,” in International workshop on security measurements and metrics (MetriSec), New York, NY, USA: ACM Press, 2010, pp. 1–8. doi: 10.1145/1853919.1853930. Author copy: https://logicalhacking.com/publications/kohler.ea-caching-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[21]

A. D. Brucker, H. Petritsch, and S. G. Weber, “Attribute-based encryption with break-glass,” in Workshop in information security theory and practice (WISTP), P. Samarati, M. Tunstall, and J. Posegga, Eds. Heidelberg: Springer-Verlag, 2010, pp. 237–244. doi: 10.1007/978-3-642-12368-9_18. Author copy: https://logicalhacking.com/publications/brucker.ea-attribute-based-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[20]

A. D. Brucker, L. Brügger, P. Kearney, and B. Wolff, “Verified firewall policy transformations for test-case generation,” in Third international conference on software testing, verification, and validation (ICST), Los Alamitos, CA, USA: IEEE Computer Society, 2010, pp. 345–354. doi: 10.1109/ICST.2010.50. Author copy: https://logicalhacking.com/publications/brucker.ea-firewall-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[19]

A. D. Brucker and D. Hutter, “Information flow in disaster management systems,” in International conference on availability, reliability and security (ARES), Los Alamitos, CA, USA: IEEE Computer Society, 2010, pp. 156–163. doi: 10.1109/ARES.2010.107. Author copy: https://logicalhacking.com/publications/brucker.ea-information-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[18]

A. D. Brucker and H. Petritsch, “Idea: Efficient evaluation of access control constraints,” in International symposium on engineering secure software and systems (ESSoS), F. Massacci, D. Wallach, and N. Zannone, Eds. Heidelberg: Springer-Verlag, 2010, pp. 157–165. doi: 10.1007/978-3-642-11747-3_12. Author copy: https://logicalhacking.com/publications/brucker.ea-efficient-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[17]

A. D. Brucker, A. Schaad, and C. Wolter, “Prozessmodellierung: Einbinden von Sicherheitsregeln in Geschäftsprozesse,” iX special – Sicher im Netz, vol. 3, pp. 152–155, Oct. 2010.
[Abstract | BibTeX | RIS | EndNote | Word]

[16]

A. D. Brucker and S. A. Mödersheim, “Integrating automated and interactive protocol verification (extended version),” IBM Research Zurich, RZ3750, 2009. Author copy: https://logicalhacking.com/publications/brucker.ea-integrating-2009-b/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[15]

A. D. Brucker and S. A. Mödersheim, “Integrating automated and interactive protocol verification,” in Workshop on formal aspects in security and trust (FAST 2009), P. Degano and J. Guttman, Eds. Heidelberg: Springer-Verlag, 2009, pp. 248–262. doi: 10.1007/978-3-642-12459-4_18. An extended version of this paper is available as IBM Research Technical Report, RZ3750.. Author copy: https://logicalhacking.com/publications/brucker.ea-integrating-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[14]

M. Kohler, A. D. Brucker, and A. Schaad, “ProActive Caching: Generating caching heuristics for business process environments,” in International conference on computational science and engineering (CSE), vol. 3, Los Alamitos, CA, USA: IEEE Computer Society, 2009, pp. 207–304. doi: 10.1109/CSE.2009.177. Author copy: https://logicalhacking.com/publications/kohler.ea-proactive-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[13]

A. D. Brucker, A. Schaad, and C. Wolter, “Prozessmodellierung: Einbinden von Sicherheitsregeln in Geschäftsprozesse,” iX, vol. 3, pp. 118–121, Mar. 2009. Eine aktualisierte Version des Artikels ist im iX special – Sicher im Netz (Oktober 2010) erschienen.
[Abstract | BibTeX | RIS | EndNote | Word]

[12]

A. D. Brucker, H. Petritsch, and A. Schaad, “Delegation assistance,” in IEEE international symposium on policies for distributed systems and networks (POLICY), Jul. 2009, pp. 84–91. doi: 10.1109/POLICY.2009.35. Author copy: https://logicalhacking.com/publications/brucker.ea-delegation-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[11]

A. D. Brucker and H. Petritsch, “Extending access control models with break-glass,” in ACM symposium on access control models and technologies (SACMAT), B. Carminati and J. Joshi, Eds. New York, NY, USA: ACM Press, 2009, pp. 197–206. doi: 10.1145/1542207.1542239. Author copy: https://logicalhacking.com/publications/brucker.ea-extending-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[10]

A. D. Brucker, L. Brügger, and B. Wolff, “Model-based firewall conformance testing,” in Testcom/FATES 2008, K. Suzuki and T. Higashino, Eds. Heidelberg: Springer-Verlag, 2008, pp. 103–118. doi: 10.1007/978-3-540-68524-1_9. Author copy: https://logicalhacking.com/publications/brucker.ea-model-based-2008/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[9]

A. D. Brucker and J. Doser, “Metamodel-based UML notations for domain-specific languages,” in 4th international workshop on software language engineering (ATEM 2007), J. M. Favre, D. Gasevic, R. Lämmel, and A. Winter, Eds. Nashville, USA, 2007. Author copy: https://logicalhacking.com/publications/brucker.ea-metamodel-2007/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[8]

A. D. Brucker and B. Wolff, “Test-sequence generation with HOL-TestGen – with an application to firewall testing,” in TAP 2007: Tests and proofs, B. Meyer and Y. Gurevich, Eds. Heidelberg: Springer-Verlag, 2007, pp. 149–168. doi: 10.1007/978-3-540-73770-4_9. Author copy: https://logicalhacking.com/publications/brucker.ea-test-sequence-2007/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[7]

A. D. Brucker, J. Doser, and B. Wolff, “An MDA framework supporting OCL,” Electronic Communications of the EASST, vol. 5, 2006, doi: 10.14279/tuj.eceasst.5.45. Author copy: https://logicalhacking.com/publications/brucker.ea-mda-2006-b/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[6]

A. D. Brucker, J. Doser, and B. Wolff, “A model transformation semantics and analysis methodology for SecureUML,” ETH Zurich, 524, 2006. Author copy: https://logicalhacking.com/publications/brucker.ea-transformation-2006-b/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[5]

A. D. Brucker, J. Doser, and B. Wolff, “A model transformation semantics and analysis methodology for SecureUML,” in MoDELS 2006: Model driven engineering languages and systems, O. Nierstrasz, J. Whittle, D. Harel, and G. Reggio, Eds. Heidelberg: Springer-Verlag, 2006, pp. 306–320. doi: 10.1007/11880240_22. An extended version of this paper is available as ETH Technical Report, no. 524.
[Abstract | DOI | BibTeX | RIS | EndNote | Word]

[4]

A. D. Brucker and B. Wolff, “A verification approach for applied system security,” International Journal on Software Tools for Technology (STTT), vol. 7, no. 3, pp. 233–247, 2005, doi: 10.1007/s10009-004-0176-3. Author copy: https://logicalhacking.com/publications/brucker.ea-verification-2005/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[3]

A. D. Brucker and B. Wolff, “A case study of a formalized security architecture,” Electronic Notes in Theoretical Computer Science, vol. 80, pp. 24–40, 2003, doi: 10.1016/S1571-0661(04)80807-7. Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS’03). Author copy: https://logicalhacking.com/publications/brucker.ea-case-2003/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[2]

A. D. Brucker, F. Rittinger, and B. Wolff, “A CVS-Server security architecture — concepts and formal analysis,” Albert-Ludwigs-Universität Freiburg, 182, 2002. Author copy: https://logicalhacking.com/publications/brucker.ea-cvs-server-2002-b/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[1]

A. D. Brucker, F. Rittinger, and B. Wolff, “The CVS-server case study: A formalized security architecture,” in FM-TOOLS 2002, D. Haneberg, G. Schellhorn, and W. Reif, Eds. Augsburg: University Augsburg, 2002, pp. 47–52. Available as Technical Report, University Augsburg, number 2002–11.. Author copy: https://logicalhacking.com/publications/brucker.ea-cvs-server-2002/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

Formal Methods

Formal methods are an important technique that helps to build safe, secure, and reliable systems. Since his studies [brucker:verifikation:2000], Achim Brucker is developing formal techniques (e.g., verification and testing) and tools (e.g., HOL-OCL) [brucker.ea:semantics:2009, brucker.ea:extensible:2008-b, brucker.ea:hol-ocl:2008 brucker:interactive:2007], HOL-TestGen [brucker.ea:theorem-prover:2012, brucker.ea:hol-testgen:2010], HOL-Z [brucker.ea:hol-z:2003, brucker.ea:verification:2005]) as well as applying them to real world problems (e.g., [brucker.ea:verification:2005, brucker.ea:firewall:2010, altenhofen.ea:issues:2010]). Focus areas of his work are specification-based testing (e.g., [brucker.ea:theorem-prover:2012, brucker.ea:test-sequence:2007, brucker.ea:symbolic:2005]), formal semantics and verification of object-oriented languages and systems (e.g., [brucker.ea:semantics:2009, brucker.ea:extensible:2008-b, brucker.ea:featherweight:2012, brucker.ea:ocl-null:2009, brucker:interactive:2007, brucker.ea:hol-ocl-book:2006, brucker.ea:ocl-testing:2010]), and the integration of formal methods into model-driven development (including UML/OCL-based approaches, e.g., [wahler.ea:efficient:2010, brucker.ea:mda:2006-b, brucker.ea:transformation:2006] as well as business-process-driven approaches, e.g., [compagna.ea:bp-compliance:2013]). More recently, he started on (formal) application security testing approaches that combine static (i.e., SAST) and dynamic (i.e., DAST) aspects to tackle the challenges of modern programming languages and programming paradigms.

[-] Publications
(Click To Expand)

[98]

A. D. Brucker, I. Ait-Sadoune, N. Méric, and B. Wolff, “Parametric ontologies in formal software engineering,” Science of Computer Programming, 2025, doi: 10.1016/j.scico.2024.103231. Author copy: https://logicalhacking.com/publications/brucker.ea-parametric-ontologies-2025/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[97]

D. Marmsoler and A. D. Brucker, “A deep embedding of Solidity in Isabelle/HOL,” Formal Aspects of Computing (FAC), 2025, doi: 10.1145/3700601. Author copy: https://logicalhacking.com/publications/marmsoler.ea-isabelle-solidity-2025/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[96]

M. Broy et al., “Does every computer scientist need to know formal methods?” Formal Aspects of Computing (FAC), 2025, doi: 10.1145/3670795. Author copy: https://logicalhacking.com/publications/broy.ea-fm-in-cs-education-2025/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[95]

[94]

[93]

A. D. Brucker, N. Méric, and B. Wolff, “Isabelle/DOF,” Archive of Formal Proofs, Jan. 2024. https://www.isa-afp.org/entries/Isabelle_DOF.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-isabelle-dof-afp-2024/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[92]

A. D. Brucker and A. Stell, “(Extended) Interval Analysis,” Archive of Formal Proofs, Jan. 2024. https://www.isa-afp.org/entries/Interval_Analysis.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-afp-2024/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[91]

A. D. Brucker, T. Cameron-Burke, and A. Stell, “Formally verified interval arithmetic and its application to program verification,” 2024. doi: 10.1145/3644033.3644370. Author copy: https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-2024/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[90]

A. D. Brucker, I. Ait-Sadoune, N. Méric, and B. Wolff, “Using deep ontologies in formal software engineering,” in International conference on rigorous state based methods (ABZ 2023), U. Glässer and D. Méry, Eds. Heidelberg: Springer-Verlag, 2023. Author copy: https://logicalhacking.com/publications/brucker.ea-deep-ontologies-2023/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[89]

[88]

A. D. Brucker and A. Stell, “Verifying feedforward neural networks for classification in Isabelle/HOL,” in Formal methods (FM 2023), M. Chechik, J.-P. Katoen, and M. Leucker, Eds. Heidelberg: Springer-Verlag, 2023. doi: 10.1007/978-3-031-27481-7_24. Author copy: https://logicalhacking.com/publications/brucker.ea-feedforward-nn-verification-2023/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[87]

A. D. Brucker, “Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML,” Archive of Formal Proofs, Jul. 2022. https://www.isa-afp.org/entries/Nano_JSON.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker-nano-json-2022/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[86]

D. Marmsoler and A. D. Brucker, “Conformance testing of formal semantics using grammar-based fuzzing,” in TAP 2022: Tests and proofs, L. Kovacs and K. Meinke, Eds. Heidelberg: Springer-Verlag, 2022. Author copy: https://logicalhacking.com/publications/marmsoler.ea-conformance-2022/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[85]

D. Marmsoler and A. D. Brucker, “A denotational semantics of Solidity in Isabelle/HOL,” in Software engineering and formal methods (SEFM), R. Calinescu and C. Pasareanu, Eds. Heidelberg: Springer-Verlag, 2021. Author copy: https://logicalhacking.com/publications/marmsoler.ea-solidity-semantics-2021/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[84]

[83]

[82]

[81]

[80]

[79]

[78]

M. Foster, A. D. Brucker, R. G. Taylor, and J. Derrick, “A formal model of extended finite state machines,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Extended_Finite_State_Machines.html, Formal proof development. Author copy: https://logicalhacking.com/publications/foster.ea-efsm-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[77]

M. Foster, A. D. Brucker, R. G. Taylor, and J. Derrick, “Inference of extended finite state machines,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html, Formal proof development. Author copy: https://logicalhacking.com/publications/foster.ea-efsm-inference-2020/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[76]

[75]

[74]

[73]

A. D. Brucker and M. Herzberg, “A formally verified model of web components,” in Formal aspects of component software (FACS), S.-S. Jongmans and F. Arbab, Eds. Heidelberg: Springer-Verlag, 2020. doi: 10.1007/978-3-030-40914-2_3. Author copy: https://logicalhacking.com/publications/brucker.ea-web-components-2019/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[72]

A. D. Brucker, G. Daniel, and F. Jouault, Eds., 19th international workshop on OCL and textual modeling, OCL 2019. proceedings, vol. 2513. CEUR-WS.org, 2019.
[Abstract | BibTeX | RIS | EndNote | Word]

[71]

A. D. Brucker and B. Wolff, “Using ontologies in formal developments targeting certification,” in Integrated formal methods (iFM), W. Ahrendt and S. L. T. Tarifa, Eds. Heidelberg: Springer-Verlag, 2019. doi: 10.1007/978-3-030-34968-4_4. Author copy: https://logicalhacking.com/publications/brucker.ea-ontologies-certification-2019/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[70]

M. Foster, A. D. Brucker, R. G. Taylor, S. North, and J. Derrick, “Incorporating data into EFSM inference,” in Software engineering and formal methods (SEFM), P. C. Ölveczky and G. Salaün, Eds. Heidelberg: Springer-Verlag, 2019, pp. 257–272. doi: 10.1007/978-3-030-30446-1_14. Author copy: https://logicalhacking.com/publications/foster.ea-incorporating-2019/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[69]

A. D. Brucker and B. Wolff, “Isabelle/DOF: Design and implementation,” in Software engineering and formal methods (SEFM), P. C. Ölveczky and G. Salaün, Eds. Heidelberg: Springer-Verlag, 2019, pp. 275–292. doi: 10.1007/978-3-030-30446-1_15. Author copy: https://logicalhacking.com/publications/brucker.ea-isabelledof-2019/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[68]

[67]

M. Foster, R. G. Taylor, A. D. Brucker, and J. Derrick, “Formalising extended finite state machine transition merging,” in ICFEM, J. S. Dong and J. Sun, Eds. Heidelberg: Springer-Verlag, 2018, pp. 373–387. doi: 10.1007/978-3-030-02450-5. Author copy: https://logicalhacking.com/publications/foster.ea-efsm-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[66]

[65]

A. D. Brucker, I. Ait-Sadoune, P. Crisafulli, and B. Wolff, “Using the Isabelle ontology framework: Linking the formal with the informal,” in Conference on intelligent computer mathematics (CICM), Heidelberg: Springer-Verlag, 2018. doi: 10.1007/978-3-319-96812-4_3. Author copy: https://logicalhacking.com/publications/brucker.ea-isabelle-ontologies-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[64]

[63]

A. D. Brucker and M. Herzberg, “Formalizing (web) standards: An application of test and proof,” in TAP 2018: Tests and proofs, C. Dubois and B. Wolff, Eds. Heidelberg: Springer-Verlag, 2018, pp. 159–166. doi: 10.1007/978-3-319-92994-1_9. Author copy: https://logicalhacking.com/publications/brucker.ea-standard-compliance-testing-2018/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[62]

[61]

[60]

A. D. Brucker and B. Wolff, “Monadic sequence testing and explicit test-refinements,” in TAP 2016: Tests and proofs, B. K. Aichernig and C. A. Furia, Eds. Heidelberg: Springer-Verlag, 2016. doi: 10.1007/978-3-319-41135-4_2. Author copy: https://logicalhacking.com/publications/brucker.ea-monadic-sequence-testing-2016/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[59]

A. D. Brucker et al., “HOL-TestGen 1.8.0 user guide,” Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, 1586, Apr. 2016. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-testgen-2016/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[58]

A. D. Brucker, J. Cabot, and A. S.-B. Herrera, Eds., 16th international workshop on OCL and textual modeling, OCL 2016, saint-malo, france, october 2, 2016. proceedings, vol. 1756. CEUR-WS.org, 2016.
[Abstract | BibTeX | RIS | EndNote | Word]

[57]

A. D. Brucker, F. Tuong, and B. Wolff, “Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5,” LRI, Univ Paris Sud, CNRS, Centrale Supélec, Université Paris-Saclay, France, 1582, Sep. 2015. Author copy: https://logicalhacking.com/publications/brucker.ea-formal-semantics-ocl-2.5-2015/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[56]

A. D. Brucker, O. Havle, Y. Nemouchi, and B. Wolff, “Testing the IPC protocol for a real-time operating system,” in Working conference on verified software: Theories, tools, and experiments, A. Gurfinkel and S. A. Seshia, Eds. Heidelberg: Springer-Verlag, 2015. doi: 10.1007/978-3-319-29613-5_3. Author copy: https://logicalhacking.com/publications/brucker.ea-ipc-testing-2015/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[55]

A. D. Brucker, M. Egea, M. Gogolla, and F. Tuong, Eds., 15th international workshop on OCL and textual modeling, OCL 2015, ottawa, canada, september 28, 2015. proceedings, vol. 1512. CEUR-WS.org, 2015.
[Abstract | BibTeX | RIS | EndNote | Word]

[54]

[53]

[52]

A. D. Brucker, C. Dania, G. Georg, and M. Gogolla, Eds., 14th international workshop on OCL and textual modeling, OCL 2014, valencia, spain, september 30, 2014. proceedings, vol. 1285. CEUR-WS.org, 2014.
[Abstract | BibTeX | RIS | EndNote | Word]

[51]

A. D. Brucker, F. Tuong, and B. Wolff, “Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5,” Archive of Formal Proofs, Jan. 2014. https://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-featherweight-2014/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[50]

[49]

A. D. Brucker, A. Feliachi, Y. Nemouchi, and B. Wolff, “Test program generation for a microprocessor: A case-study,” in TAP 2013: Tests and proofs, L. Viganò and M. Veanes, Eds. Heidelberg: Springer-Verlag, 2013, pp. 76–95. doi: 10.1007/978-3-642-38916-0_5. Author copy: https://logicalhacking.com/publications/brucker.ea-test-program-generation-2013/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[48]

[47]

A. D. Brucker, D. Longuet, F. Tuong, and B. Wolff, “On the semantics of object-oriented data structures and path expressions (extended version),” Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, 1565, 2013. Author copy: https://logicalhacking.com/publications/brucker.ea-path-expressions-2013-b/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[46]

A. D. Brucker, D. Longuet, F. Tuong, and B. Wolff, “On the semantics of object-oriented data structures and path expressions,” in Proceedings of the MODELS 2013 OCL workshop (OCL 2013), 2013, vol. 1092, pp. 23–32. An extended version of this paper is available as LRI Technical Report 1565.. Author copy: https://logicalhacking.com/publications/brucker.ea-path-expressions-2013/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[45]

A. D. Brucker and B. Wolff, “On theorem prover-based testing,” Formal Aspects of Computing (FAC), vol. 25, no. 5, pp. 683–721, 2013, doi: 10.1007/s00165-012-0222-y. Author copy: https://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[44]

A. D. Brucker and B. Wolff, “Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL,” in Workshop on OCL and textual modelling (OCL 2012), 2012, pp. 19–24. doi: 10.1145/2428516.2428520. The semantics for the Boolean operators proposed in this paper was adopted by the OCL 2.4 standard.. Author copy: https://logicalhacking.com/publications/brucker.ea-featherweight-2012/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[43]

A. D. Brucker and J. Julliand, Eds., Tests and proofs - 6th international conference, TAP 2012, praque, czech republic, mai 31 – june 1, 2012. proceedings, vol. 7305. Heidelberg: Springer-Verlag, 2012. doi: 10.1007/978-3-642-30473-6.
[Abstract | DOI | BibTeX | RIS | EndNote | Word]

[42]

A. D. Brucker, L. Brügger, M. P. Krieger, and B. Wolff, “HOL-TestGen 1.7.0 user guide,” Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, 1551, Apr. 2012. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-testgen-2012/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[41]

[40]

M. P. Krieger and A. D. Brucker, “Extending OCL operation contracts with objective functions,” Electronic Communications of the EASST, vol. 44, 2011, doi: 10.14279/tuj.eceasst.44.662. Author copy: https://logicalhacking.com/publications/krieger.ea-objective-functions-2011/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[39]

A. D. Brucker, M. P. Krieger, D. Longuet, and B. Wolff, “A specification-based test case generation method for UML/OCL,” in MoDELS workshops, J. Dingel and A. Solberg, Eds. Heidelberg: Springer-Verlag, 2010, pp. 334–348. doi: 10.1007/978-3-642-21210-9_33. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.. Author copy: https://logicalhacking.com/publications/brucker.ea-ocl-testing-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[38]

M. Altenhofen and A. D. Brucker, “Practical issues with formal specifications: Lessons learned from an industrial case study,” in International workshop on formal methods for industrial critical systems (FMICS), S. Kowalewski and M. Roveri, Eds. Heidelberg: Springer-Verlag, 2010, pp. 17–32. doi: 10.1007/978-3-642-15898-8_2. Author copy: https://logicalhacking.com/publications/altenhofen.ea-issues-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[37]

[36]

M. Wahler, D. Basin, A. D. Brucker, and J. Koehler, “Efficient analysis of pattern-based constraint specifications,” Software and Systems Modeling, vol. 9, no. 2, pp. 225–255, Apr. 2010, doi: 10.1007/s10270-009-0123-6. Author copy: https://logicalhacking.com/publications/wahler.ea-efficient-2010/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[35]

[34]

A. D. Brucker, M. P. Krieger, and B. Wolff, “Extending OCL with null-references,” in Models in software engineering, S. Gosh, Ed. Heidelberg: Springer-Verlag, 2009, pp. 261–275. doi: 10.1007/978-3-642-12261-3_25. Selected best papers from all satellite events of the MoDELS 2009 conference.. Author copy: https://logicalhacking.com/publications/brucker.ea-ocl-null-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[33]

[32]

[31]

A. D. Brucker and B. Wolff, “HOL-TestGen: An interactive test-case generation framework,” in Fundamental approaches to software engineering (FASE09), M. Chechik and M. Wirsing, Eds. Heidelberg: Springer-Verlag, 2009, pp. 417–420. doi: 10.1007/978-3-642-00593-0_28. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[30]

A. D. Brucker and B. Wolff, “Semantics, calculi, and analysis for object-oriented specifications,” Acta Informatica, vol. 46, no. 4, pp. 255–284, Jul. 2009, doi: 10.1007/s00236-009-0093-8. Author copy: https://logicalhacking.com/publications/brucker.ea-semantics-2009/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[29]

A. D. Brucker and B. Wolff, “An extensible encoding of object-oriented data models in HOL,” Journal of Automated Reasoning, vol. 41, pp. 219–249, 2008, doi: 10.1007/s10817-008-9108-3. Author copy: https://logicalhacking.com/publications/brucker.ea-extensible-2008-b/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[28]

A. D. Brucker and B. Wolff, “Tutorial: Analyzing UML/OCL models with HOL-OCL,” presented at the MoDELS 2008, Toulouse, France, Sep. 28, 2008. Author copy: https://logicalhacking.com/publications/talk-brucker.ea-analyzing-2008/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[27]

[26]

A. D. Brucker and B. Wolff, “Extensible universes for object-oriented data models,” in ECOOP 2008 – object-oriented programming, J. Vitek, Ed. Heidelberg: Springer-Verlag, 2008, pp. 438–462. doi: 10.1007/978-3-540-70592-5_19. Author copy: https://logicalhacking.com/publications/brucker.ea-extensible-2008/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[25]

A. D. Brucker, L. Brügger, and B. Wolff, “Verifying test-hypotheses: An experiment in test and proof,” Electronic Notes in Theoretical Computer Science, vol. 220, no. 1, pp. 15–27, 2008, doi: 10.1016/j.entcs.2008.11.003. Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008). Author copy: https://logicalhacking.com/publications/brucker.ea-verifying-2008/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[24]

A. D. Brucker and B. Wolff, “HOL-OCL – A Formal Proof Environment for UML/OCL,” in Fundamental approaches to software engineering (FASE08), J. Fiadeiro and P. Inverardi, Eds. Heidelberg: Springer-Verlag, 2008, pp. 97–100. doi: 10.1007/978-3-540-78743-3_8. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-ocl-2008/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[23]

A. D. Brucker, “An interactive proof environment for object-oriented specifications,” PhD thesis, ETH Zurich, 2007. ETH Dissertation No. 17097.. Author copy: https://logicalhacking.com/publications/brucker-interactive-2007/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[22]

[21]

A. D. Brucker, J. Doser, and B. Wolff, “Semantic issues of OCL: Past, present, and future,” Electronic Communications of the EASST, vol. 5, 2006, doi: 10.14279/tuj.eceasst.5.46. Author copy: https://logicalhacking.com/publications/brucker.ea-semantic-2006-b/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[20]

[19]

[18]

A. D. Brucker and B. Wolff, “A package for extensible object-oriented data models with an application to IMP++,” in International workshop on software verification and validation (SVV 2006), A. Roychoudhury and Z. Yang, Eds. Seattle, USA, 2006. Author copy: https://logicalhacking.com/publications/brucker.ea-package-2006/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[17]

[16]

[15]

A. D. Brucker and B. Wolff, “Interactive testing using HOL-TestGen,” in Formal approaches to testing of software, W. Grieskamp and C. Weise, Eds. Heidelberg: Springer-Verlag, 2005. doi: 10.1007/11759744_7. Author copy: https://logicalhacking.com/publications/brucker.ea-interactive-2005/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[14]

[13]

[12]

A. D. Brucker and B. Wolff, “Symbolic test case generation for primitive recursive functions,” in Formal approaches to testing of software, J. Grabowski and B. Nielsen, Eds. Heidelberg: Springer-Verlag, 2004, pp. 16–32. doi: 10.1007/b106767. Author copy: https://logicalhacking.com/publications/brucker.ea-symbolic-2005/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[11]

[10]

A. D. Brucker, F. Rittinger, and B. Wolff, “HOL-Z 2.0: A proof environment for Z-specifications,” Journal of Universal Computer Science, vol. 9, no. 2, pp. 152–172, Feb. 2003, doi: 10.3217/jucs-009-02-0152. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-z-2003/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[9]

A. D. Brucker and B. Wolff, “Using theory morphisms for implementing formal methods tools,” in Types for proof and programs, H. Geuvers and F. Wiedijk, Eds. Heidelberg: Springer-Verlag, 2003, pp. 59–77. doi: 10.1007/3-540-39185-1_4. Author copy: https://logicalhacking.com/publications/brucker.ea-embedding-2003/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[8]

[7]

A. D. Brucker and B. Wolff, “A note on design decisions of a formalization of the OCL,” Albert-Ludwigs-Universität Freiburg, 168, Jan. 2002. Author copy: https://logicalhacking.com/publications/brucker.ea-note-2002/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[6]

A. D. Brucker and B. Wolff, “A proposal for a formal OCL semantics in Isabelle/HOL,” in Theorem proving in higher order logics (TPHOLs), V. A. Carreño, C. A. Muñoz, and S. Tahar, Eds. Heidelberg: Springer-Verlag, 2002, pp. 99–114. doi: 10.1007/3-540-45685-6_8. Author copy: https://logicalhacking.com/publications/brucker.ea-proposal-2002/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[5]

A. D. Brucker, S. Friedrich, F. Rittinger, and B. Wolff, “HOL-Z 2.0: A proof environment for Z-specifications,” in FM-TOOLS 2002, D. Haneberg, G. Schellhorn, and W. Reif, Eds. Augsburg: University Augsburg, 2002, pp. 33–38. Available as Technical Report, University Augsburg, number 2002–11.. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-z-2002/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[4]

A. D. Brucker and B. Wolff, “HOL-OCL: Experiences, consequences and design choices,” in UML 2002: Model engineering, concepts and tools, J.-M. Jézéquel, H. Hussmann, and S. Cook, Eds. Heidelberg: Springer-Verlag, 2002, pp. 196–211. doi: 10.1007/3-540-45800-X_17. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-ocl-2002/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[3]

[2]

[1]

A. D. Brucker, “Verifikation von Dividierern mit Word-Level-Decision-Diagrams,” Diplomarbeit, Albert-Ludwigs-Universität Freiburg, Freiburg, 2000. Author copy: https://logicalhacking.com/publications/brucker-verifikation-2000/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

Software Engineering

Since the beginning of his PhD studies, Achim Brucker is working on formal (e.g., [brucker.ea:theorem-prover:2012, brucker.ea:hol-z:2003, brucker.ea:featherweight:2012, brucker.ea:hol-ocl:2008, brucker.ea:extensible:2008-b]) and applied (e.g., [monakova.ea:securing:2012, kohler.ea:caching:2010, marienfeld.ea:usdl-security:2012, probst.ea:soknos:2010, braune.ea:service-oriented:2011, brucker.ea:extending:2009]) aspects of software engineering and system engineering. In general, he is interested in (formal) software processes that help to build safe, secure, and reliable systems. In particular, he worked on the formal semantics of object-oriented languages [brucker.ea:featherweight:2012, brucker.ea:ocl-null:2009, brucker.ea:extensible:2008-b, brucker:interactive:2007] as well as developing formal verification techniques for object-oriented systems [brucker.ea:hol-ocl:2008, brucker:interactive:2007, brucker.ea:semantics:2009]. Moreover, he worked on theorem-prover-based testing techniques [brucker.ea:hol-testgen:2012, brucker.ea:theorem-prover:2012, brucker.ea:testing:2001, brucker.ea:hol-testgen:2010] that allow for combining verification (i.e., formal proofs) and testing. He integrated these techniques into model-driven development processes (e.g., [wahler.ea:model-driven:2006-b brucker.ea:transformation:2006]) and CASE tools [brucker.ea:mda:2006-b], e.g., for enterprise systems [brucker.ea:securebpmn:2012]. This also includes meta-model-based language engineering [brucker.ea:metamodel:2007] to integrate security aspects in standard modeling languages such as SecureUML (extending UML) [brucker.ea:extending:2009, brucker.ea:transformation:2006] or SecureBPMN (extending BPMN) [brucker:securebpmn:2013, brucker.ea:securebpmn:2012, brucker.ea:framework:2013, compagna.ea:bp-compliance:2013]. Moreover, he works on various techniques for securing service-oriented and cloud-based systems [braune.ea:service-oriented:2011, marienfeld.ea:usdl-security:2012, probst.ea:soknos:2010, brucker.ea:checking:2001, brucker.ea:efficient:2010, brucker.ea:secure:2012] as well as business-process-driven systems [compagna.ea:bp-compliance:2013, brucker.ea:securebpmn:2012, monakova.ea:securing:2012, kohler.ea:caching:2010].

[-] Publications
(Click To Expand)

[120]

[119]

[118]

[117]

[116]

[115]

[114]

[113]

[112]

[111]

[110]

[109]

[108]

[107]

[106]

[105]

[104]

[103]

[102]

[101]

[100]

[99]

[98]

[97]

[96]

[95]

[94]

[93]

[92]

[91]

[90]

[89]

[88]

[87]

[86]

R. Bill, A. D. Brucker, J. C. M. Gogolla, A. Vallecillo, and E. D. Wilink, “Workshop in OCL and textual textual modelling: Report on recent trends and panel discussion,” in STAF 2017 workshops, 2017, vol. 10748, pp. 157–165. Author copy: https://logicalhacking.com/publications/bill.ea-recent-developments-2017/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[85]

[84]

[83]

[82]

[81]

[80]

[79]

[78]

A. D. Brucker et al., “Recent developments in OCL and textual modelling,” in Proceedings of the international workshop on OCL and textual modeling (OCL 2016), 2016, vol. 1756, pp. 157–165. Author copy: https://logicalhacking.com/publications/brucker.ea-recent-developments-2016/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[77]

[76]

[75]

[74]

[73]

[72]

[71]

[70]

A. D. Brucker et al., “Panel discussion: Proposals for improving OCL,” in Proceedings of the MODELS 2014 OCL workshop (OCL 2014), 2014, vol. 1285, pp. 83–99. Author copy: https://logicalhacking.com/publications/brucker.ea-ocl-community-2014/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[69]

[68]

[67]

[66]

[65]

[64]

[63]

[62]

[61]

[60]

[59]

[58]

[57]

[56]

[55]

[54]

A. D. Brucker et al., “Report on the Aachen OCL meeting,” in Proceedings of the MODELS 2013 OCL workshop (OCL 2013), 2013, vol. 1092, pp. 103–111. Author copy: https://logicalhacking.com/publications/brucker.ea-summary-aachen-2013/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[53]

[52]

[51]

[50]

[49]

[48]

[47]

[46]

[45]

[44]

S. Braune et al., “A service-oriented architecture for emergency management systems,” in Software engineering 2011 – workshopband, Feb. 2011, vol. P–184, pp. 225–232. Innovative Systeme zur Unterstützung der zivilen Sicherheit: Architekturen und Gestaltungskonzepte.. Author copy: https://logicalhacking.com/publications/braune.ea-service-oriented-2011/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[43]

[42]

[41]

[40]

[39]

[38]

[37]

[36]

[35]

[34]

[33]

[32]

[31]

[30]

[29]

[28]

[27]

[26]

[25]

[24]

[23]

[22]

[21]

[20]

M. Wahler, J. Koehler, and A. D. Brucker, “Model-driven constraint engineering,” Electronic Communications of the EASST, vol. 5, 2006, doi: 10.14279/tuj.eceasst.5.44. Author copy: https://logicalhacking.com/publications/wahler.ea-model-driven-2006-b/
[Abstract | PDF | DOI | BibTeX | RIS | EndNote | Word]

[19]

[18]

[17]

[16]

[15]

[14]

[13]

[12]

[11]

[10]

[9]

[8]

[7]

[6]

[5]

[4]

[3]

[2]

A. D. Brucker and B. Wolff, “Testing distributed component based systems using UML/OCL,” in Informatik 2001, Nov. 2001, vol. 1, pp. 608–614. Author copy: https://logicalhacking.com/publications/brucker.ea-testing-2001/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

[1]

A. D. Brucker and B. Wolff, “Checking OCL constraints in distributed systems using J2EE/EJB,” Albert-Ludwigs-Universität Freiburg, 157, Jul. 2001. Author copy: https://logicalhacking.com/publications/brucker.ea-checking-2001/
[Abstract | PDF | BibTeX | RIS | EndNote | Word]

Hardware

During his computer science studies, Achim Brucker specialized in hardware verification and microsystems engineering. Parallel to his studies the worked at a company and developed test tools for embedded systems. He still enjoys designing own hardware and programming embedded systems in his spare time.

[-] Publications
(Click To Expand)

[2]

[1]

Information Security

[-] Publications(Click To Expand)

Formal Methods

[-] Publications(Click To Expand)

Software Engineering

[-] Publications(Click To Expand)

Hardware

[-] Publications(Click To Expand)

[-] Publications
(Click To Expand)

[-] Publications
(Click To Expand)

[-] Publications
(Click To Expand)

[-] Publications
(Click To Expand)