SMT-Based Bounded Model Checking for Embedded ANSI-C Software (2009)
Cordeiro, Lucas, Fischer, Bernd, Marques-Silva, Joao
Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the...
Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking (2009)
Cordeiro, Lucas, Fischer, Bernd, Marques-Silva, Joao
The complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. In...
Industrial-Strength Formally Certified SAT Solving (2009)
Darbari, Ashish, Fischer, Bernd, Marques-Silva, Joao
Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the railways, avionics, and...
Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking (2009)
Cordeiro, Lucas, Fischer, Bernd, Marques-Silva, Joao
The complexity of software in embedded systems has increased significantly over the last years so that software verification now plays an important role in ensuring the overall product quality. In...
A New Approach for Motion Correction in SPECT Imaging (2009)
Hanno Schumacher, Bernd Fischer
Abstract. Due to the long imaging times in SPECT, patient motion is inevitable and constitutes a serious problem for any reconstruction algorithm. The measured inconsistent projection data lead to...
Curvature Based Registration with Applications (2009)
To Mr-mammography, Bernd Fischer, Jan Modersitzki
1 Introduction Registration of 2D or 3D medical images is necessary in order to study the evolution of a pathology of a patient, or to take full advantage of the complementary information coming from...
A Communication Term for the Combined Registration and Segmentation (2009)
Konstantin Ens, Jens Von Berg, Bernd Fischer
Abstract — Accurate image registration is a necessary prerequisite for many diagnostic and therapy planning procedures where complementary information from different images has to be combined. The...
SMT-Based Bounded Model Checking for Embedded ANSI-C Software (2009)
Cordeiro, Lucas, Fischer, Bernd, Marques-Silva, Joao
Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the...
Iterative Reconstruction of SPECT Images using Adaptive Multi-Level Refinement (2009)
Hanno Schumacher, Stefan Heldmann, Eldad Haber, Bernd Fischer
Abstract. We present a novel method for iterative reconstruction of high resolution images. Our method is based on the observation that constant regions in an image can be represented at much lower...
Cordeiro, Lucas, Fischer, Bernd, Chen, Huan, Marques-Silva, Joao
In recent days, the complexity of software has increased significantly in embedded products in such a way that the verification of Embedded Software (ESW) now plays an important role to ensure the...
Adding Concrete Syntax to a Prolog-Based Program Synthesis System (Extended Abstract) (2008)
Abstract. Program generation and transformation systems manipulate large, parameterized object language fragments. Support for user-definable concrete syntax makes this easier but is typically...
c○Springer-Verlag Data Resampling for Path Based Clustering (2008)
Bernd Fischer, Joachim M. Buhmann
Abstract. Path Based Clustering assigns two objects to the same cluster if they are connected by a path with high similarity between adjacent objects on the path. In this paper, we propose a fast...
Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where most probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Basir, Nurlida, Denney, Ewen, Fischer, Bernd
Formal methods can in principle provide the highest levels of assurance of code safety by providing formal proofs as explicit evidence for the assurance claims. However, the proofs are often complex...
Formal Safety Certification of Auto-Generated Aerospace Software (2008)
Code generators can address many of the increasing demands placed on software in the aerospace industry, yet trust in the code produced by commercial generators is notoriously difficult to achieve...
Ewen Denney, Bernd Fischer, Johann Schumann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
Mathematics Meets Medicine: An Alignment Story (2008)
Bernd Fischer, Jan Modersitzki
Medical imaging has come a long way since 1895, when Wilhelm Conrad Röntgen discovered x-rays. More than a century later, the phrase “going for a scan ” can refer to a multitude of different...
Bernd Fischer, Johann Schumann
Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability...
Franz F. Roos, Riko Jacob, Jonas Grossmann, Bernd Fischer, Joachim M. Buhmann, Wilhelm Gruissem, ...
Motivation: Tandem mass spectrometry allows for high throughput identification of complex protein samples. Searching tandem mass spectra against sequence databases is the main analysis method...
Nils Papenberg, Hanno Schumacher, Stefan Heldmann, Stefan Wirtz, Silke Bommersheim, Konstantin Ens, ...
Abstract. In the last decades there has been tremendous research towards the design of fully automatic non-rigid registration schemes. However, apart from the ITK based implementation of Rueckerts...
Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where most probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Image Fusion and Registration – a Variational Approach (2008)
Bernd Fischer, Jan Modersitzki
Summary. Image fusion or registration is central to many challenges in medical imaging today and has a vast range of applications. The purpose of this paper is to give an introduction to intensity...
Stefan Heldmann, Oliver Mahnke, Daniel Potts, Jan Modersitzki, Bernd Fischer
Abstract. In this paper we present a novel method for computing the Mutual Information of images using recently developed non-equidistant fast Fourier-transform (NFFT) techniques. Standard approaches...
Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code (2008)
Basir, Nurlida, Denney, Ewen, Fischer, Bernd
We present an approach to systematically derive safety cases for automatically generated code from information collected during a formal, Hoare-style safety certification of the code. This safety...
Rao, Rajnish P, Fischer, Bernd, Seshagiri, Polani B
Leukemia inhibitory factor (LIF) is a pleiotropic IL-6 family cytokine and its maternal uterine expression is critical for mouse blastocyst implantation. In the golden hamster (Mesocricetus auratus),...
Bernd Fischer, Volker Roth, Joachim M. Buhmann, Jonas Grossmann, Sacha Baginsky, Wilhelm Gruissem, ...
De novo Sequencing of peptides is a challenging task in proteome research. While there exist reliable DNA-sequencing methods, the highthroughput de novo sequencing of proteins by mass spectrometry is...
Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models (2008)
Karen A. Huyser, Kevin H. Knuth, Bernd Fischer, Domhnull Granquist-fraser, Arsen R. Hajian
Astronomical objects known as planetary nebulae (PNe) consist of a shell of gas expelled by an aging star. In cases where the gas shell can be assumed to be ellipsoidal, the PN can be easily modeled...
Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Rao, Rajnish P, Fischer, Bernd, Seshagiri, Polani B
Leukemia inhibitory factor (LIF) is a pleiotropic IL-6 family cytokine and its maternal uterine expression is critical for mouse blastocyst implantation. In the golden hamster (Mesocricetus auratus),...
National Aeronautics and Space Administration Preface (2008)
Johann Schumann, Hamed Jafari, Tom Pressburger, Ewen Denney, Wray Buntine, Bernd Fischer
Program synthesis is the systematic, automatic construction of efficient executable code from high-level declarative specifications. AutoBayes is a fully automatic program synthesis system for the...
Time-series alignment by non-negative multiple generalized canonical correlation analysis (2007)
Fischer, Bernd, Roth, Volker, Buhmann, Joachim M
Abstract Background Quantitative analysis of differential protein expressions requires to align temporal elution measurements from liquid chromatography coupled to mass spectrometry (LC/MS). We...
Thomas Baar, Bernd Fischer, Dirk Fuchs, Abt Softwaretechnologie, Tu Braunschweig, ...
Abstract. We describe a combination of the NORA/HAMMR software component retrieval tool and the ILF system which provides the necessary infrastructure to apply different first-order theorem provers...
Solving Software Reuse Problems with Theorem Provers (2007)
Thomas Baar, Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
Abstract. For a challenging application, the software component retrieval, we present a powerful solution by combining two systems. The NORA/HAMMR-tool handles all aspects concerning with the logical...
Solving Software Reuse Problems with Theorem Provers (2007)
Thomas Baar, Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
In NORA/HAMMR, we investigate the application of automated theorem provers to retrieve software components based on their formal specifications. The problem pro le has major impacts on the problem...
Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Bernd Fischer, Carsten Hammer, Werner Struckmann
A large number of scanner generators have been developed. Since they are restricted to the longestmatch rule, they are unsuitable for an incremental environment. We present the ALADIN system, which...
Orthogonal polynomial wavelets (2007)
Bernd Fischer, Woula Themistoclakis
Recently Fischer and Prestin presented a unied approach for the construction of polynomial wavelets. In particular, they characterized those parameter sets which lead to orthogonal scaling functions....
Bernd Fischer, Thomas Zöller, Joachim M. Buhmann, Rheinische Friedrich
Abstract. Most cost function based clustering or partitioning methods measure the compactness of groups of data. In contrast to this picture of a point source in feature space, some data sources are...
Autobayes: A system for synthesizing data analysis programs (2007)
Bernd Fischer, Johann Schumann
Statistical approaches to data analysis, which use methods from probability theory and numerical analysis, are well-founded but difficult to implement: the development of a statistical data analysis...
From Orthogonal Polynomials To Iteration Schemes For Linear Systems: CG and CR Revisited (2007)
Large systems of linear equations arise frequently in numerical analysis and are the basis of many models in engineering and other applied sciences. This note provides a study for the solution of...
Adding Concrete Syntax to a Prolog-Based Program Synthesis System (Extended Abstract) (2007)
Bernd Fischer and Eelco Visser 1 RIACS / NASA Ames Research Center Moffett Field, CA 94035, USA fisch@email.arc.nasa.gov 2 Institute of Information and Computing Sciences, Universiteit Utrecht 3508...
Fast Curvature Based Registration of (2007)
Bernd Fischer, Jan Modersitzki
We introduce a new non-linear registration model based on a curvature type regularizer. We show that ane linear transformations belong to the kernel of this regularizer. Consequently, an additional...
Abstract Background We develop a probabilistic model for combining kernel matrices to predict the function of proteins. It extends previous approaches in that it can handle multiple labels which...
Differential expression of oxygen-regulated genes in bovine blastocysts (2007)
Harvey, Alexandra Juanita, Kirstein, M., Kind, Karen Lee, Fischer, Bernd, Thompson, Jeremy Gilbert E.
Low oxygen conditions (2%) during post-compaction culture of bovine blastocysts improve embryo quality, which is associated with a small yet significant increase in the expression of glucose...
Differential expression of oxygen-regulated genes in bovine blastocysts (2007)
Harvey, Alexandra Juanita, Kirstein, M., Kind, Karen Lee, Fischer, Bernd, Thompson, Jeremy Gilbert E.
Low oxygen conditions (2%) during post-compaction culture of bovine blastocysts improve embryo quality, which is associated with a small yet significant increase in the expression of glucose...
Tonack, S., Kind, Karen Lee, Thompson, Jeremy Gilbert E., Wobus, A. M., Fischer, Bernd, Santos, A. N.
Copyright © 2007 by The Endocrine Society
Tonack, S., Kind, Karen Lee, Thompson, Jeremy Gilbert E., Wobus, A. M., Fischer, Bernd, Santos, A. N.
Copyright © 2007 by The Endocrine Society
Roos, Franz F., Jacob, Riko, Grossmann, Jonas, Fischer, Bernd, Buhmann, Joachim M., Gruissem, Wilhelm, ...
Motivation: Tandem mass spectrometry allows for high-throughput identification of complex protein samples. Searching tandem mass spectra against sequence databases is the main analysis method...
An Empirical Evaluation of Automated Theorem Provers in Software Certification (2006)
Denney, Ewen, Fischer, Bernd, Schumann, Johann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
An Empirical Evaluation of Automated Theorem Provers in Software Certification (2006)
Denney, Ewen, Fischer, Bernd, Schumann, Johann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
An Empirical Evaluation of Automated Theorem Provers in Software Certification (2006)
Denney, Ewen, Fischer, Bernd, Schumann, Johann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e.,...
Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e.,...
Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e.,...
architectures through significant improvements in performance and in power consumption. (2006)
An Assura geometry extraction and Spectre re-simulation flow to simulate Shallow Trench Isolation (STI) stress effects in analogue circuits
Christoph Benzmüller, Bernd Fischer, Geoff Sutcliffe, Held At, Christoph Benzmüller, Bernd Fischer, ...
on the Implementation of Logics
Semi-supervised lc/ms alignment for differential proteomics (2006)
Bernd Fischer, Jonas Grossmann, Volker Roth, Wilhelm Gruissem, Sacha Baginsky, Joachim M. Buhmann
doi:10.1093/bioinformatics/btl219
Semi-supervised LC/MS alignment for differential proteomics (2006)
Fischer, Bernd, Grossmann, Jonas, Roth, Volker, Gruissem, Wilhelm, Baginsky, Sacha, Buhmann, Joachim M.
Motivation: Mass spectrometry (MS) combined with high-performance liquid chromatography (LC) has received considerable attention for high-throughput analysis of proteomes. Isotopic labeling...
Profiles of raindrop size distributions as retrieved by microrain radars (2005)
Peters,Gerhard, Fischer,Bernd, Münster,Hans, Clemens,M., Wagner,A.
Data of vertically pointing microrain radars (MRRs), located at various sites around the Baltic Sea, were analyzed for a period of several years. From the Doppler spectra profiles of drop size...
Profiles of raindrop size distributions as retrieved by microrain radars (2005)
Peters, Gerhard, Fischer, Bernd, Münster, Hans, Clemens, M., Wagner, A.
Data of vertically pointing microrain radars (MRRs), located at various sites around the Baltic Sea, were analyzed for a period of several years. From the Doppler spectra profiles of drop size...
Certifiable program generation (2005)
Abstract. Code generators based on template expansion techniques are easier to build than purely deductive systems but do not guarantee the same level of assurance: instead of providing...
Practical Proof Checking for Program Certification (2005)
Geoff Sutcliffe, Ewen Denney, Bernd Fischer
Program certification aims to provide explicit evidence that a program meets a specified level of safety. This evidence must be independently reproducible and verifiable. We have developed a system,...
A program certification assistant based on fully automated theorem provers (2005)
We describe a certification assistant to support formal safety proofs for programs. It is based on a graphical user interface that hides the low-level details of first-order automated theorem provers...
Special Interest Group on Artificial Intelligence (SIGART) (2005)
Ewen Denney, Bernd Fischer, Mark Jones, Dieter Hutter, Ewen Denney
This volume contains the position papers presented at the Workshop on Software Certificate Management (SoftCe-
Practical Proof Checking for Program Certification (2005)
Geoff Sutcliffe, Ewen Denney, Bernd Fischer
Program certification aims to provide explicit evidence that a program meets a specified level of safety. This evidence must be independently reproducible and verifiable. We have developed a system,...
Practical Proof Checking for Program Certification (2005)
Geoff Sutcliffe, Ewen Denney, Bernd Fischer
Program certification aims to provide explicit evidence that a program meets a specified level of safety. This evidence must be independently reproducible and verifiable. We have developed a system,...
Practical Proof Checking for Program Certification (2005)
Geoff Sutcliffe, Ewen Denney, Bernd Fischer
Program certification aims to provide explicit evidence that a program meets a specified level of safety. This evidence must be independently reproducible and verifiable. We have developed a system,...
A program certification assistant based on fully automated theorem provers (2005)
We describe a certification assistant to support formal safety proofs for programs. It is based on a graphical user interface that hides the lowlevel details of first-order automated theorem provers...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2004)
Fischer, Bernd, Knuth, Kevin, Hajian, Arsen, Schumann, Johann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented and...
Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software (2004)
Denney, Ewen, Fischer, Bernd, Schumann, Johann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2004)
Fischer, Bernd, Knuth, Kevin, Hajian, Arsen, Schumann, Johann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented and...
Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models (2004)
Huyser, Karen A., Knuth, Kevin H., Fischer, Bernd, Schumann, Johann, Granquist-Fraser, Domhnull, Hajian, Arsen R.
Astronomical objects known as planetary nebulae (PNe) consist of a shell of gas expelled by an aging star. In cases where the gas shell can be assumed to be ellipsoidal, the PN can be easily modeled...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2004)
Fischer, Bernd, Knuth, Kevin, Hajian, Arsen, Schumann, Johann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented and...
Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software (2004)
Denney, Ewen, Fischer, Bernd, Schumann, Johann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2004)
Fischer, Bernd, Knuth, Kevin, Hajian, Arsen, Schumann, Johann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented and...
Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models (2004)
Huyser, Karen A., Knuth, Kevin H., Fischer, Bernd, Schumann, Johann, Granquist-Fraser, Domhnull, Hajian, Arsen R.
Astronomical objects known as planetary nebulae (PNe) consist of a shell of gas expelled by an aging star. In cases where the gas shell can be assumed to be ellipsoidal, the PN can be easily modeled...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2004)
Fischer, Bernd, Knuth, Kevin, Hajian, Arsen, Schumann, Johann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented and...
Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software (2004)
Denney, Ewen, Fischer, Bernd, Schumann, Johann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2004)
Fischer, Bernd, Knuth, Kevin, Hajian, Arsen, Schumann, Johann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented and...
Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models (2004)
Huyser, Karen A., Knuth, Kevin H., Fischer, Bernd, Schumann, Johann, Granquist-Fraser, Domhnull, Hajian, Arsen R.
Astronomical objects known as planetary nebulae (PNe) consist of a shell of gas expelled by an aging star. In cases where the gas shell can be assumed to be ellipsoidal, the PN can be easily modeled...
Insulin acts via mitogen-activated protein kinase phosphorylation in rabbit blastocysts (2004)
Santos, Anne Navarrete, Tonack, Sarah, Kirstein, Michaela, Pantaleon, Marie, Kaye,Peter, Fischer,Bernd
The addition of insulin during in vitro culture has beneficial effects on rabbit preimplantation embryos leading to increased cell proliferation and reduced apoptosis. We have previously described...
Insulin acts via mitogen-activated protein kinase phosphorylation in rabbit blastocysts (2004)
Santos, Anne Navarrete, Tonack, Sarah, Kirstein, Michaela, Pantaleon, Marie, Kaye,Peter, Fischer,Bernd
The addition of insulin during in vitro culture has beneficial effects on rabbit preimplantation embryos leading to increased cell proliferation and reduced apoptosis. We have previously described...
Adding Assurance to Automatically Generated Code (2004)
Ewen Denney, Bernd Fischer, Johann Schumann
Code to estimate position and attitude of a spacecraft or aircraft belongs to the most safety-critical parts of flight software. The complex underlying mathematics and abundance of design details...
Using automated theorem provers to certify auto-generated aerospace software (2004)
Ewen Denney, Bernd Fischer, Johann Schumann
Abstract. We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which...
Adding Assurance to Automatically Generated Code (2004)
Ewen Denney, Bernd Fischer, Johann Schumann
Abstract — Code to estimate position and attitude of a spacecraft or aircraft belongs to the most safety-critical parts of flight software. The complex underlying mathematics and abundance of...
Retrofitting the AutoBayes program synthesis system with concrete object syntax (2004)
Bernd Fischer, Eelco Visser, See Also, Bernd Fischer, Eelco Visser, Bernd Fischer, ...
Abstract. AUTOBAYES is a fully automatic, schema-based program synthesis system for statistical data analysis applications. Its core component is a schema library, i.e., a collection of generic code...
Retrofitting the AutoBayes program synthesis system with concrete object syntax (2004)
See Also, Bernd Fischer, Bernd Fischer, Bernd Fischer, Eelco Visser, Eelco Visser, ...
Abstract. AUTOBAYES is a fully automatic, schema-based program synthesis system for statistical data analysis applications. Its core component is a schema library, i.e., a collection of generic code...
Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software (2004)
Ewen Denney, Bernd Fischer, Johann Schumann
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then...
gamm header will be provided by the publisher Large (2004)
Bernd Fischer, Jan Modersitzki
scale problems arising from image registration
Adding Assurance to Automatically Generated Code (2004)
Ewen Denney, Bernd Fischer, Johann Schumann
Abstract — Code to estimate position and attitude of a spacecraft or aircraft belongs to the most safety-critical parts of ¤ight software. The complex underlying mathematics and abundance of...
Clustering with the connectivity kernel (2004)
Bernd Fischer, Volker Roth, Joachim M. Buhmann
Clustering aims at extracting hidden structure in dataset. While the problem of finding compact clusters has been widely studied in the literature, extracting arbitrarily formed elongated structures...
Bernd Fischer, Jan Modersitzki
Abstract Image registration is central to many challenges in medical imaging today. It has a vast range of applications. The purpose of this note is twofold. First, we review some of the most...
Paola Pocar, Robert Augustin, Fulvio Gandolfi, Bernd Fischer
Alkylphenolic compounds are a widespread family of xenoestrogens. High concentrations of these substances are present in sewage sludge that is spread on arable land and pasture as fertilizer. Because...
AutoBayes: A System for Generating Data Analysis Programs from Statistical Models (2003)
Fischer, Bernd, Schumann, Johann
Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability...
AutoBayes: A System for Generating Data Analysis Programs from Statistical Models (2003)
Fischer, Bernd, Schumann, Johann
Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability...
AutoBayes: A System for Generating Data Analysis Programs from Statistical Models (2003)
Fischer, Bernd, Schumann, Johann
Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability...
Correctness of Source-Level Safety Policies (2003)
Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be established externally. In this paper...
Automatic Derivation of Statistical Algorithms: The EM Family and Beyond (2003)
Gray, Alexander G., Fischer, Bernd, Schumann, Johann, Buntine, Wray
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Correctness of Source-Level Safety Policies (2003)
Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be established externally. In this paper...
Automatic Derivation of Statistical Algorithms: The EM Family and Beyond (2003)
Gray, Alexander G., Fischer, Bernd, Schumann, Johann, Buntine, Wray
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
An Application of a Mathematical Blood Flow Model (2003)
Breuss, Michael, Meister, Andreas, Fischer, Bernd
Mathematical models of blood flow are inevitably embedded in models of human thermoregulation because they take the role of the most significant heat distributor in models of the human thermal system...
Correctness of Source-Level Safety Policies (2003)
Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be established externally. In this paper...
Automatic Derivation of Statistical Algorithms: The EM Family and Beyond (2003)
Gray, Alexander G., Fischer, Bernd, Schumann, Johann, Buntine, Wray
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Certification Support for Automatically Generated Programs (2003)
Johann Schumann, Bernd Fischer, Mike Whalen, Jon Whittle
Although autocoding techniques promise large gains in software development productivity, their “real-world ” application has been limited, particularly in safety-critical domains. Often, the...
Correctness of Source-Level Safety Policies (2003)
Abstract. Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be established externally. In...
Certification Support for Automatically Generated Programs (2003)
Johann Schumann, Bernd Fischer, Mike Whalen
Although autocoding techniques promise large gains in software development productivity, their “real-world ” application has been limited, particularly in safety-critical domains. Often, the...
Automatic Derivation of the Multinomial PCA Algorithm (2003)
Wray Buntine, Bernd Fischer, Alexander G. Gray
Machine learning has reached a point where probabilistic methods can be understood as variations, extensions, and combinations of a small set of abstract themes, e.g., as di#erent instances of the EM...
Certification Support for Automatically Generated Programs (2003)
Johann Schumann, Bernd Fischer, Mike Whalen, Jon Whittle
Although autocoding techniques promise large gains in software development productivity, their "real-world" application has been limited, particularly in safety-critical domains. Often, the...
Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond (2003)
Bernd Fischer, Arsen Hajian, Kevin Knuth, Johann Schumann
AUTOBAYES is a fully automatic program synthesis system for the data analysis domain.
Certification Support for Automatically Generated Programs (2003)
Johann Schumann, Bernd Fischer, Mike Whalen, Jon Whittle
Although autocoding techniques promise large gains in software development productivity, their “real-world ” application has been limited, particularly in safety-critical domains. Often, the...
Visual field representations and locations of visual areas V1/2/3 in human visual cortex (2003)
Robert F. Dougherty, Volker M. Koch, Alyssa A. Brewer, Bernd Fischer, Brian A. Wandell
The position, surface area and visual field representation of human visual areas V1, V2 and V3 were measured using fMRI in 7 subjects (14 hemispheres). Cortical visual field maps of the central 12...
Clustering with the Connectivity Kernel (2003)
Bernd Fischer, Volker Roth, Joachim M. Buhmann
Clustering aims at extracting hidden structure in dataset. While the problem of finding compact clusters has been widely studied in the literature, extracting arbitrarily formed elongated structures...
Path-based clustering for grouping of smooth curves and texture segmentation (2003)
Bernd Fischer, Student Member, Joachim M. Buhmann
Abstract—Perceptual Grouping organizes image parts in clusters based on psychophysically plausible similarity measures. We propose a novel grouping method in this paper, which stresses...
Automatic derivation of statistical data analysis algorithms: Planetary nebulae and beyond (2003)
Bernd Fischer, Arsen Hajian, Kevin Knuth, Johann Schumann
Abstract. AUTOBAYES is a fully automatic program synthesis system for the data analysis domain. Its input is a declarative problem description in form of a statistical model; its output is documented...
FLIRT: A flexible image registration toolbox (2003)
Bernd Fischer, Jan Modersitzki
1 Introduction In the last two decades, computerized non-rigid image registration has playedan increasingly important role in medical imaging, see for example Maintz & Viergever [13], Fitzpatrick...
Synthesizing Certified Code (2002)
Whalen, Michael, Schumann, Johann, Fischer, Bernd
Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain...
Synthesizing Certified Code (2002)
Whalen, Michael, Schumann, Johann, Fischer, Bernd
Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain...
Synthesizing Certified Code (2002)
Whalen, Michael, Schumann, Johann, Fischer, Bernd
Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain...
Deduction-based software component retrieval [Elektronische Ressource] / (2002)
Erscheinungsjahr an der Haupttitelstelle: 2001.
Michael Whalen, Johann Schumann, Bernd Fischer
Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator...
Automatic derivation of statistical algorithms: The EM family and beyond (2002)
Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Automatic derivation of statistical algorithms: The EM family and beyond (2002)
Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Automatic Derivation of Statistical Algorithms: (2002)
The Em Family, Alexander G. Gray, Bernd Fischer, Johann Schumann, Wray Buntine
Machine learning has reached a point where most probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different...
Synthesizing certified code (2002)
Michael Whalen, Johann Schumann, Bernd Fischer
Abstract. Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies...
Deduction-Based Software Component Retrieval (2001)
Deduction-based software component retrieval is a software reuse technique that uses formal specifications as component descriptors and as search keys; matching components are identified using an...
Interpreting abstract interpretations in membership equational logic (2001)
We present a logical framework in which abstract interpretations can be naturally speci ed and then veried. Our approach is based on membership equational logic which extends equational logics by...
A Super Fast Registration Algorithm (2001)
Bernd Fischer And, Bernd Fischer, Jan Modersitzki
Image registration is an often encountered problem in digital imaging, in particular in medical imaging. In most applications simple rigid deformations are not satisfactory and complex, non-rigid and...
The Unsteady Thermoregulation of Premature Infants - A Model and Its Application (2001)
Michael Breuß, Bernd Fischer, Andreas Meister
The focus of our interest is the temporal development of the temperature distribution within a premature infant inside an incubator.
Modellierung zeitabhängiger Magnetfelder in Kristallzüchtungsanordnungen / (2001)
Erlangen, Nürnberg, Universiẗat, Diss., 2001.
Cellular localization of human relaxin-like factor in the cyclic endometrium and placenta (2001)
Hombach-Klonisch, Sabine, Seeger, Sven, Tscheudschilsuren, Gerelsul, Buchmann, Jörg, Huppertz, Berthold, Seliger, Gregor, ...
We have studied the cellular localization of the relaxin-like factor (RLF) in the histologically normal cyclic endometrium collected from days 3–26 of the menstrual cycle. RLF transcripts and...
Molecular Remodeling of Members of the Relaxin Family During Primate Evolution (2001)
Klonisch, Thomas, Froehlich, Christine, Tetens, Frank, Fischer, Bernd, Hombach-Klonisch, Sabine
Employing comparative analysis of the cDNA-coding sequences of the unique preprorelaxin of the Afro-lorisiform Galago crassicaudatus and the Malagasy lemur Varecia variegata and the relaxin-like...
An Application of the Finite Volume Method to the Thermoregulation of Infants (2000)
Reihe F, Reihe A Preprints, Reihe B Berichte, Reihe C Mathematische, Modelle Simulation, Reihe D Elektrische, ...
A mathematical model is developed and used for a computer simulation of the thermoregulation of premature infants. We propose a finite volume technique for the solution of the associated partial...
Integrating deduction techniques in a software reuse application (1999)
Thomas Baar, Bernd Fischer, Dirk Fuchs
We investigate the application of automated deduction techniques to retrieve software components based on their formal specifications. The application profile has major impacts on the problem solving...
An Integration of Deductive Retrieval into Deductive Synthesis (1999)
Bernd Fischer Riacs, Bernd Fischer, Jon Whittle
Deductive retrieval and deductive synthesis are two conceptually closely related software development methods which apply theorem proving techniques to support the construction of correct programs....
Specification-Based Browsing of Software Component Libraries (1999)
. Specification-based retrieval provides exact content-oriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any...
Towards Automated Synthesis of Data Mining Programs (1999)
Wray Buntine, Bernd Fischer, Thomas Pressburger
Code synthesis is routinely used in industry to generate GUIs, form filling applications, and database support code and is even used with COBOL. In this paper we consider the question of whether code...
Transformation Systems at NASA Ames (1999)
Wray Buntine Bernd, Bernd Fischer, Klaus Havelund, Michael Lowry, Tom Pressburger, Steve Roach, ...
In this paper, we describe the experiences of the Automated Software Engineering Group at the NASA Ames Research Center in the development and application of three different transformation systems....
An Integration of Deductive Retrieval into Deductive Synthesis (1999)
Deductive retrieval and deductive synthesis are two conceptually closely related software development methods which apply theorem proving techniques to support the construction of correct programs....
Transformation Systems at NASA Ames (1999)
Wray Buntine, Bernd Fischer, Klaus Havelund, Michael Lowry, Tom Pressburger, Steve Roach, ...
In this paper, we describe the experiences of the Automated Software Engineering Group at the NASA Ames Research Center in the development and application of three different transformation systems....
Expression of relaxin-like factor is down-regulated in human testicular Leydig cell neoplasia (1999)
Klonisch, Thomas, Ivell, Richard, Balvers, Marga, Kliesch, Sabine, Fischer, Bernd, Bergmann, Martin, ...
In addition to their role in steroidogenesis in the male, testicular Leydig cells constitutively express large amounts of the peptide relaxin-like factor (RLF), also known as Ley-IL. The Leydig...
Specification-Based Browsing of Software Component Libraries (1998)
Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
Specification-based retrieval provides exact content-oriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any...
Specification-Based Browsing of Software Component Libraries (1998)
Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
Specification-based retrieval provides exact content-oriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any...
Specification-Based Browsing of Software Component Libraries (1998)
Bernd Fischer Abt, Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
Specification-based retrieval provides exact contentoriented access to component libraries but requires too much deductive power. Specification-based browsing evades this bottleneck by moving any...
Leipzig, Univ., Diss., 1998.
Wavelets based on orthogonal polynomials (1997)
Bernd Fischer, J Urgen Prestin
Abstract. We present a unified approach for the construction of polynomial wavelets. Our main tool are orthogonal polynomials. With the help of their properties we devise schemes for the construction...
NORA/HAMMR: Making deduction-based software component retrieval practical (1997)
Johann Schumann, Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig
Deduction-based software component retrieval uses preand postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very simple...
Bernd Fischer, Gregor Snelting
Reuse by contract is the application of formal methods to software reuse: software components are associated with contracts---formal models of their functional behaviour---and administered,...
Wavelets Based on Orthogonal Polynomials (1997)
We present a unified approach for the construction of polynomial wavelets. Our main tool are orthogonal polynomials. With the help of their properties we devise schemes for the construction of time...
Wavelets based on orthogonal polynomials (1997)
Abstract. We present a unified approach for the construction of polynomial wavelets. Our main tool is orthogonal polynomials. With the help of their properties we devise schemes for the construction...
Münster (Westfalen), Univ., Diss., 1994.
Seiler, Petra, Fischer, Bernd, Lindenau, Antje, Beier, Henning M.
The commercial polychlorinated biphenyl (PCB) formulation Aroclor 1260 (4 mg/kg body weight), technical grade dichlorodiphenyltrichloroethane (DDT; 3 mg) and Lindane (γ-hexachlorocyclohexane;...
Effects of persistent chlorinated hydrocarbons on reproductive tissues in female rabbits (1994)
Lindenau, Antje, Fischer, Bernd, Seiler, Petra, Beier, Henning M.
The female rabbit was used to study (i) accumulation of lipophilic chlorinated hydrocarbons in genital tract tissues and (ii) subsequent morphological and functional effects after longterm low-dose...
Resolution for Feature Logic (1993)
Bernd Fischer, Ag Softwaretechnologie, Tu Braunschweig
: A common approach to combine the object-oriented and logic programming paradigms is to formulate a set of inference rules for an object logic. We show how resolution is expressed using the full...
ALADIN: A Scanner Generator for Incremental Programming Environments (1992)
Bernd Fischer, Carsten Hammer, Werner Struckmann
Summary: A large number of scanner generators have been developed. Since they are restricted to the longest match rule they are unsuitable for an incremental environment. We present the...
Zugl.: Essen, Univ., Diss. : 1989.
Geomedizinische Aspekte der Mekong-Schistosomiasis in der VDR Laos / (1988)
Fischer, Carla., Fischer, Bernd.
Rostock, Univ., Diss. A, 1988 (Nicht f.d. Austausch).
Zum Entwurf frequenzselektiver Bauelemente der Mikroakustik. (1988)
Dresden, Techn. Univ., Diss. B, 1989 (Nicht f.d. Austausch).
Berlin, Humboldt-Univ., Diss. A, 1987 (Nicht f.d. Austausch).
Quantitative aspects of protein synthesis in non-cultured and cultured rabbit blastocysts (1987)
Jung, Thomas, Fischer, Bernd, Beier, Henning M.
Day 4 rabbit blastocysts were cultured in Ham's F-10 medium supplemented either with homologous serum or uterine flushings. Development was assessed by leucine and methionine incorporation at 24 h...
Thesis (doctoral)--Rheinische Friedrich-Wilhelms-Universität Bonn, 1985.
Räumliche Bestimmungsfaktoren des Wahlverhaltens in europäischen Kontexten [microform] / (1984)
Thesis (doctoral)--Ruprecht-Karls-Universität Heidelberg, 1984.
Metalle in der Glasschmelztechnik / (1983)
Karl-Marx-Stadt, Techn. Hochsch., Diss. A, 1983 (Nicht für den Austausch).
Degree granted by Dept. of German.
Köln, Univ., Rechtswiss. Fak., Diss., 1976.
Hannover, Techn. Univ., Fak. f. Mathematik u. Naturwiss., Diss. 1974.
Leipzig, Univ., Bereich Medizin, Diss. A, 1973. (Nicht f. d. Austausch.).
Ein automatischer Scanner für Kernspurplatten. (1972)
Marburg, Univ., Fachbereich Physik, Diss. 1972.
Komplikationen bei Operationen im Kiefer- und Gesichtsbereich in Allgemeinnarkose. (1969)
Leipzig, Med. F., Diss. v. 13. Jan. 1969 (Nicht f. d. Aust.).
Leipzig, Med. F., Diss. v. 19. Dez. 1967 (Nicht f. d. Aust.).
Die Problematik der Handelsumlenkungen und des Ursprungsbegriffes in einer Freihandelszone. (1961)
Thèse Sciences économiques sociales, Fribourg/S, 1961.
Die Problematik der Handelsumlenkungen und des Ursprungsbegriffes in einer Freihandelszone. (1961)
Diss.--Freiburg.
Die Problematik der Handelsumlenkungen und des Ursorungsbegriffes in einer Freihande zone. (1961)
Diss.--Fribourg.
Nürnberg, Hochsch. für Wirtschafts- und Sozialwiss., Diss., 1960.
Nürnberg, H. f. Wirtsch.- u. Sozialwiss., Diss. v. 23. Nov. 1960.
Thèse rer. pol., Nuremberg, 1960.
NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical
Bernd Fischer, Abt Softwaretechnologie, Tu Braunschweig, Johann Schumann
Deduction-based software component retrieval uses pre- and postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very...
The AutoBayes Program Synthesis System - System Description
Bernd Fischer, Thomas Pressburger, Grigore Rosu, Johann Schumann
interpretation is used as an e#cient mechanism to evaluate range constraints suchasx#0orx6= 0 which occur in the conditions of many rewrite rules. AutoBayes implements as a rewrite system a...