The University of Southampton
Warning! Your browser is out-of-date and not compatible with this website. Please download a new secure and faster browser to view this website correctly.

Research

Publications

Denney, Ewen, Fischer, Bernd and Schumann, Johann (2006) An Empirical Evaluation of Automated Theorem Provers in Software Certification. International Journal on Artificial Intelligence Tools, 15, (1), 81-107.

Fischer, Bernd and Schumann, Johann (2003) AutoBayes: A System for Generating Data Analysis Programs from Statistical Models. Journal of Functional Programming, 13, (3), 483-508.

Denney, Ewen and Fischer, Bernd (2003) Correctness of Source-Level Safety Policies. In, FME 2003: Formal Methods, Pisa, Italy, 08 - 14 Sep 2003. Springer Verlag, 894-913.

Fischer, Bernd, Knuth, Kevin, Hajian, Arsen and Schumann, Johann (2004) Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond. In, 23rd International Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, Jackson Hole, Wyoming, USA, 03 - 08 Aug 2003. AIP Press, 276-291.

Gray, Alexander G., Fischer, Bernd, Schumann, Johann and Buntine, Wray (2003) Automatic Derivation of Statistical Algorithms: The EM Family and Beyond. In, Neural Information Processing Systems 15, Vancouver, BC, 09 - 14 Dec 2002. MIT Press, 689-696.

Fischer, Bernd and Schumann, Johann (1997) SETHEO Goes Software Engineering: Application of ATP to Software Reuse. In, 14th International Conference on Automated Deduction, Townsville, Springer Verlag, 65-68.

Whalen, Michael, Schumann, Johann and Fischer, Bernd (2002) AutoBayes/CC --- Combining Program Synthesis with Automatic Code Certification (System Description). In, 18th International Conference on Automated Deduction, Copenhagen, 27 - 30 Jul 2002. Springer Verlag, 290-294.

Denney, Ewen, Fischer, Bernd and Schumann, Johann (2004) Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software. In, Second International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Springer Verlag, 198-212.

Fischer, Bernd, Knuth, Kevin, Hajian, Arsen and Schumann, Johann (2004) Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond. In, 23rd International Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, Jackson Hole, Wyoming, USA, 03 - 08 Aug 2003. AIP Press, 276-291.

Huyser, Karen A., Knuth, Kevin H., Fischer, Bernd, Schumann, Johann, Granquist-Fraser, Domhnull and Hajian, Arsen R. (2004) Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models. In, Twentyfourth International Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, Garching bei München, Germany, 25 - 30 Jul 2004. AIP Press, 135-142.

Whalen, Michael, Schumann, Johann and Fischer, Bernd (2002) Synthesizing Certified Code. In, FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, 22 - 24 Jul 2002. Springer Verlag, 431-450.

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2008) Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code. In, International Workshop on the Certification of Safety-Critical Software Controlled Systems (SafeCert '08), Budapest, Hungary, Elsevier.

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2008) Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information. In, The 27th International Conference on Computer Safety, Reliability and Security (SAFECOMP'08), Newcastle upon Tyne, UK, 22 - 25 Sep 2008.

Cordeiro, Lucas, Fischer, Bernd, Chen, Huan and Marques-Silva, Joao (2009) Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. In, The 6th International Conference on Embedded Software and Systems, HangZhou, Zhejiang, China, 25 - 27 May 2009.

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2009) SMT-Based Bounded Model Checking for Embedded ANSI-C Software.

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2009) SMT-Based Bounded Model Checking for Embedded ANSI-C Software. At 24th IEEE/ACM International Conference on Automated Software Engineering, , Auckland, New Zealand, 16 - 20 Nov 2009.

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2009) Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking.

Cordeiro, Lucas, Fischer, Bernd, Chen, Huan and Marques-Silva, Joao (2009) Formal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. At 6th IEEE International Conference on Embedded Systems and Software (ICESS-09)

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2009) SMT-Based Bounded Model Checking for Embedded ANSI-C Software. At 24th IEEE/ACM International Conference on Automated Software Engineering, , Auckland, New Zealand, 16 - 20 Nov 2009.

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2010) Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. In, 17th IEEE International Conference and Workshops on Engineering of Computer-Based Systems, St. Anne's College, University of Oxford, UK, 22 - 26 Mar 2010.

Grech, Neville, Rathke, Julian and Fischer, Bernd (2010) Generating correct and efficient equality and hashing methods using JEqualityGen. In, Workshop on Generative Technologies, Paphos, Cyprus,

Cordeiro, Lucas and Fischer, Bernd (2010) Bounded Model Checking of Multi-threaded Software using SMT solvers.

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2010) Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. At 17th IEEE International Conference and Workshops on Engineering of Computer-Based Systems, St. Anne's College, University of Oxford, UK, 22 - 26 Mar 2010.

Basir, N., Denney, E. and Fischer, B. (2008) Constructing a safety case for automatically generated code from formal program verification. Computer Safety, Reliability, and Security. Proceedings 27th International Conference, SAFECOMP 2008, 249-62.

Fischer, B., Saabas, A. and Uustalu, T. (2009) Program repair as sound optimization of broken programs. 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), 165-73|xiii+333.

Egyed, A and Fischer, B (2009) Guest editors' introduction. AUTOMATED SOFTWARE ENGINEERING, 16, 1-2.

Denney, Ewen and Fischer, Bernd (2009) A verification-driven approach to traceability and documentation for auto-generated mathematical software. At ASE '09. Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, Auckland, NZ, 16 - 20 Nov 2009. , 560-564. (doi:10.1109/ASE.2009.71).

Denney, Ewen and Fischer, Bernd (2008) Explaining Verification Conditions. In, AMAST , 145-159.

Denney, Ewen and Fischer, Bernd (2008) Generating customized verifiers for automatically generated code. In, GPCE , 77-88.

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2009) Deriving Safety Cases from Automatically Constructed Proofs. In, 4th System Safety Conference 2009, London, UK, 26 - 28 Oct 2009.

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2009) Deriving Safety Cases from Machine-Generated Proofs. In, Workshop on Proof-Carrying Code and Software Certification (PCC'09), Los Angeles, California, USA,

Cordeiro, Lucas and Fischer, Bernd (2010) Bounded Model Checking of Multi-threaded Software using SMT solvers. At 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, 14 - 15 Jul 2010.

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2010) Deriving safety cases for hierarchical structure in model-based development. In, 29th International Conference on Computer Safety, Reliability and Security, Vienna, Austria, 14 - 17 Sep 2010. Springer , 68-81. (doi:10.1007/978-3-642-15651-9_6).

Grech, Neville, Fischer, Bernd and Rathke, Julian (2010) JEqualityGen: Generating Equality and Hashing Methods. At Generative Programming and Component Engineering,, Eindhoven, The , Netherlands, 10 - 13 Oct 2010. Association for Computing Machinery, 177-186.

Cordeiro, Lucas and Fischer, Bernd (2011) Verifying multi-threaded software using SMT-based context-bounded model checking. In, ICSE '11. Proceedings of the 33rd International Conference on Software Engineering, Honolulu, US, 21 - 28 May 2011. , 331-340. (doi:10.1145/1985793.1985839).

Cordeiro, Lucas, Fischer, Bernd and Marques-Silva, Joao (2012) SMT-based bounded model checking for embedded ANSI-C software. IEEE Transactions on Software Engineering, 38, (4), 957-974. (doi:10.1109/TSE.2011.59).

Morse, Jeremy, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd (2011) Context-Bounded Model Checking of LTL Properties for ANSI-C Software. In, 9th International Conference on Software Engineering and Formal Methods, Montevideo, Uruguay, 18 - 14 Nov 2011. , 302-317.

Barreto, Raimundo, Cordeiro, Lucas and Fischer, Bernd (2011) Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker.

Cordeiro, Lucas and Fischer, Bernd (2011) Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking. At International Conference on Software Engineering, Waikiki, Honolulu, Hawaii, 21 - 28 May 2011.

Cordeiro, Lucas, Morse, Jeremy, Nicole, Denis and Fischer, Bernd (2012) Context-bounded model checking with ESBMC 1.17. In, Flanagan, Cormac and König, Barbara (eds.) Tools and Algorithms for the Construction and Analysis of Systems Tools and Algorithms for the Construction and Analysis of Systems. 18th International Conference, TACAS 2012 Berlin, DE, Springer, 534-537. (Lecture Notes in Computer Science: Theoretical Computer Science and General Issues, 7214). (doi:10.1007/978-3-642-28756-5_42).

Barreto, Raimundo, Cordeiro, Lucas and Fischer, Bernd (2011) Verifying Embedded C Software with Timing Constraints using an Untimed Bounded Model Checker. At Symposium on Computing System Engineering, Florianópolis, Santa Catarina, Brazil, 07 - 11 Nov 2011.

Morse, Jeremy, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd (2011) Context-bounded model checking of LTL properties for ANSI-C software. In, Software Engineering and Formal Methods. 9th International Conference, SEFM 2011 Berlin, DE, Springer, 302-317. (Lecture Notes in Computer Science: Programming and Software Engineering, 7041). (doi:10.1007/978-3-642-24690-6_21).

Morse, Jeremy, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd (2012) Model checking LTL properties over ANSI-C programs with bounded traces. 9th International Conference on Software Engineering and Formal Methods (SEFM 2011), Montevideo, UY, 14 - 18 Nov 2011. 30pp. (doi:10.1007/s10270-013-0366-0).

Fischer, Bernd, Inverso, Omar and Parlato, Gennaro (2013) CSeq: A Sequentialization Tool for C - (Competition Contribution). In, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013 , 616-618.

Morse, Jeremy, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd (2013) Handling unbounded loops with ESBMC 1.20. In, Piterman, Nir and Smolka, Scott A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Berlin, DE, Heidelberg, DE, Springer, 619-622. (Lecture Notes in Computer Science, 7795). (doi:10.1007/978-3-642-36742-7_47).

Morse, Jeremy, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd (2013) Model checking LTL properties over C programs with bounded traces. Software and Systems Modeling, n/a, n/a. (doi:10.1007/s10270-013-0366-0).

Grech, Neville, Rathke, Julian and Fischer, Bernd (2013) Preemptive type checking in dynamically typed languages. In, 10th International Colloquium on Theoretical Aspects of Computing, Shanghai, China, 04 - 06 Sep 2013. Springer-Verlag, 195-212.

Tomasco, Ermenegildo, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) MU-CSeq: sequentialization of c programs by shared memory unwindings (competition contribution). In, TACAS (SV-COMP)

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq: a lazy sequentialization tool for c (competition contribution). In, Tools and Algorithms for the Construction and Analysis of Systems - TACAS (SV-COMP)

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Bounded model checking of multi-threaded c programs via lazy sequentialization. In, 26th International Conference on Computer Aided Verification (CAV 2014), Wien, AT, 18 - 22 Jul 2014. 18pp.

Fischer, Bernd, Inverso, Omar and Parlato, Gennaro (2013) CSeq: a concurrency pre-processor for sequential c verification tools (tool demonstration). In, 28th IEEE/ACM International Conference on Automated Software Engineering (ASE) IEEE.

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq: a lazy sequentialization tool for C. In, 20th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 05 - 13 Apr 2014. , 398-401. (doi:10.1007/978-3-642-54862-8_29).

Tomasco, Ermenegildo, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Verifying concurrent programs by memory unwinding. In, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), London, GB, 11 - 18 Apr 2015. 15pp.

Tomasco, Ermenegildo, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) MU-CSeq 0.3: Sequentialization by read-implicit and coarse-grained memory unwindings (competition contribution). In, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), London, GB, 11 - 15 Apr 2015. 3pp.

Lam Nguyen, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Unbounded Lazy-CSeq: a lazy sequentialization tool for C programs with unbounded context switches (competition contribution). In, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), London, GB, 11 - 18 Apr 2015. 3pp.

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq 0.6c: An improved lazy sequentialization tool for C (competition contribution). Southampton, GB, University of Southampton, 3pp.

Inverso, Omar, Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs. In, 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015) IEEE/ACM.

Inverso, Omar, Nguyen, Truc, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Lazy-CSeq 1.0:(Competition Contribution). , University of Southampton

Nguyen, Truc, Inverso, Omar, Tomasco, Ermenegildo, La Torre, Salvatore, Fischer, Bernd and Parlato, Gennaro (2015) Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C with unboundedly many Context Switches: (Competition Contribution). , University of Southampton

Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Lazy sequentialization for the safety verification of unbounded concurrent programs. In, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Chiba, JP, 17 - 19 Oct 2016. 16pp.

Tomasco, Ermenegildo, Nguyen Lam, Truc, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions. In, Formal Methods in Computer-Aided Design (FMCAD), Mountain View, US, 02 - 06 Oct 2016.

Tomasco, Ermenegildo, Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Separating computation from communication: a design approach for concurrent program verification. Southampton, GB, University of Southampton, 31pp.

Contact

Share this profile FacebookGoogle+TwitterWeibo

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

×