The University of Southampton

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), pp. 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), pp. 483-508.

Denney, Ewen and Fischer, Bernd, (2003) Correctness of Source-Level Safety Policies Araki, Keijiro, Gnesi, Stefania and Mandrioli, Dino (eds.) At FME 2003: Formal Methods, Italy. 08 - 14 Sep 2003. , pp. 894-913.

Fischer, Bernd, Knuth, Kevin, Hajian, Arsen and Schumann, Johann, (2004) Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond Erickson, Gary and Knuth, Kevin (eds.) At 23rd International Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, United States. 03 - 08 Aug 2003. , pp. 276-291.

Gray, Alexander G., Fischer, Bernd, Schumann, Johann and Buntine, Wray, (2003) Automatic Derivation of Statistical Algorithms: The EM Family and Beyond Becker, Suzanna, Thrun, Sebastian and Obermayer, Klaus (eds.) At Neural Information Processing Systems 15. 09 - 14 Dec 2002. , pp. 689-696.

Fischer, Bernd and Schumann, Johann, (1997) SETHEO Goes Software Engineering: Application of ATP to Software Reuse McCune, William (ed.) At 14th International Conference on Automated Deduction. , pp. 65-68.

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

Denney, Ewen, Fischer, Bernd and Schumann, Johann, (2004) Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software Basin, David and Rusinowitch, Michael (eds.) At Second International Joint Conference on Automated Reasoning (IJCAR 2004). , pp. 198-212.

Fischer, Bernd, Knuth, Kevin, Hajian, Arsen and Schumann, Johann, (2004) Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond Erickson, Gary and Knuth, Kevin (eds.) At 23rd International Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, United States. 03 - 08 Aug 2003. , pp. 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 Fischer, R. and Dose, V. (eds.) At Twentyfourth International Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, Germany. 25 - 30 Jul 2004. , pp. 135-142.

Whalen, Michael, Schumann, Johann and Fischer, Bernd, (2002) Synthesizing Certified Code Eriksson, Lars-Henrik and Lindsay, Peter A. (eds.) At FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe. 22 - 24 Jul 2002. , pp. 431-450.

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

Basir, Nurlida, Denney, Ewen and Fischer, Bernd, (2008) Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information Harrison, M.D. and Sujan, M-A. (eds.) At The 27th International Conference on Computer Safety, Reliability and Security (SAFECOMP'08), United Kingdom. 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 At The 6th International Conference on Embedded Software and Systems, China. 25 - 27 May 2009.

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

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, 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 s.n.

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, 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 At 17th IEEE International Conference and Workshops on Engineering of Computer-Based Systems, United Kingdom. 22 - 26 Mar 2010.

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

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

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, United Kingdom. 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, pp. 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, pp. 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, New Zealand. 16 - 20 Nov 2009. , pp. 560-564. (doi:10.1109/ASE.2009.71).

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

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

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

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2009) Deriving Safety Cases from Machine-Generated Proofs At Workshop on Proof-Carrying Code and Software Certification (PCC'09), United States.

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

Basir, Nurlida, Denney, Ewen and Fischer, Bernd (2010) Deriving safety cases for hierarchical structure in model-based development At 29th International Conference on Computer Safety, Reliability and Security, Austria. 14 - 17 Sep 2010. , pp. 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,, Netherlands. 10 - 13 Oct 2010. , pp. 177-186.

Cordeiro, Lucas and Fischer, Bernd (2011) Verifying multi-threaded software using SMT-based context-bounded model checking At ICSE '11. Proceedings of the 33rd International Conference on Software Engineering, United States. 21 - 28 May 2011. , pp. 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), pp. 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 At 9th International Conference on Software Engineering and Formal Methods, Uruguay. , pp. 302-317.

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

Cordeiro, Lucas and Fischer, Bernd (2011) Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking At International Conference on Software Engineering. 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 pp. 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, 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. vol. 7041, Springer., pp. 302-317. (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 At 9th International Conference on Software Engineering and Formal Methods (SEFM 2011), Uruguay. 14 - 18 Nov 2011. 30 pp. (doi:10.1007/s10270-013-0366-0).

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

Morse, Jeremy, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd, (2013) Handling unbounded loops with ESBMC 1.20 Piterman, Nir and Smolka, Scott A. (eds.) In 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. vol. 7795, Springer., pp. 619-622. (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 At 10th International Colloquium on Theoretical Aspects of Computing, China. 04 - 06 Sep 2013. , pp. 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) At 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) At 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 At 26th International Conference on Computer Aided Verification (CAV 2014), Austria. 18 - 22 Jul 2014. 18 pp.

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

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq: a lazy sequentialization tool for C At 20th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 05 - 13 Apr 2014. , pp. 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 At 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), United Kingdom. 11 - 18 Apr 2015. 15 pp.

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) At 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), United Kingdom. 11 - 15 Apr 2015. 3 pp.

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) At 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), United Kingdom. 11 - 18 Apr 2015. 3 pp.

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 At 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015).

Birch, Geoff, Fischer, Bernd and Poppleton, Michael (2015) Fast model-based fault localisation with test suites In Tests and Proofs: 9th International Conference, TAP 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 22-24, 2015. Proceedings. vol. 9154, Springer., pp. 38-57. (doi:10.1007/978-3-319-21215-9_3).

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 At 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Japan. 17 - 19 Oct 2016. 16 pp.

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 At Formal Methods in Computer-Aided Design (FMCAD), United States. 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.

Birch, Geoff, Fischer, Bernd and Poppleton, Michael (2016) Using fast model-based fault localisation to aid students in self-guided program repair and to improve assessment In ITiCSE '16: Proceedings of the 2016 ACM Conference on Innovation and Technology in Computer Science Education. ACM., pp. 168-173. (doi:10.1145/2899415.2899433).

Tomasco, Ermenegildo, Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Embedding weak memory models within eager sequentialization , Southampton, GB University of Southampton 29pp.

Morse, Jeremy, Ramalho Gadelha, Mikhail, Cordeiro, Lucas, Nicole, Denis and Fischer, Bernd (2014) ESBMC 1.22 In, Tools and Algorithms for the Construction and Analysis of Systems. 20th International Conference, TACAS 2014 Springer pp. 405-407. (Lecture Notes in Computer Science, 8413).

NGUYEN, TRUC L, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro, (2017) Lazy-CSeq 2.0: combining lazy sequentialization with abstract interpretation: (Competition contribution) Legay, Axel and Margaria, Tiziana (eds.) In Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, P. vol. 10206, Springer. 4 pp.

NGUYEN, TRUC L, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2017) Concurrent program verification with Lazy sequentialization and interval analysis In The 5th Edition of The International Conference on Networked sYStems. Springer. 15 pp, pp. 255-271. (doi:10.1007/978-3-319-59647-1_20).

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.

×