Brian Larson | Research Associate

Brian Larson

B.E.E. (1983) and M.S.C.Sci. (1995) University of Minnesota.

Contact Information
(612) 462-5188

Program correctness proofs
Architecture Analysis and Design Language (AADL)
Safety-critical systems
Medical devices
Systems engineering
Software Certification

Academic Highlights

Patent in Process:
Application 12/970,613 (Filed December 16, 2010) Automatic Programming of Rate-Adaptive Therapy Via Activity Monitoring
Patents Granted:
6,504,841        Three-dimensional interconnection geometries for multi-stage switching
                        networks using flexible ribbon cable connection between multiple planes
6,301,247        Pad and cable geometries for spring clip mounting and electrically connecting
                        flat flexible multiconductor printed circuit cables to switching chips on spaced-parallel
                        planar modules
6,215,786        Implementation of multi-stage switching networks
6,212,179        Single-type fabric card networks and method of implementing same
5,867,649        DANCE/Multitude Concurrent Computation[1]
4,833,468        Layered network[2]
4,723,242        Digital adaptive voting
4,498,177        M Out of N code checker circuit

[1]   U.S. Pat. No. 5,867,649 attempts to define from first principles, five, interrelated logics, of which the logic that does computation defines the patented process of satisfying interval temporal logic formulas with lattices of states.  The programming language DANCE was devised to support formal proofs of correctness of programs mapped onto machines with Multitude architectures to achieve speed-up unbound by Amdahl's Law.  Proving embedded program correctness builds upon the proof outline checker devised for highly-concurrent programs written in DANCE.

[2]   U.S. Pat. No. 4,833,468 defines a fault-tolerant, multistage interconnection network topology, routing algorithm, and VLSI implementation that combined requests, and de-combined responses.  Hardware implementation of combinable operations was crucial to the Multitude architecture support for concurrently-accessible data structures needed to circumvent Amdahl's Law.  Lockheed Martin used this topology for its SCI switch.  The most recent four patents relate to physical realization of this topology.

Courses Taught

NSF/FDA Scholar in Residence


SAE AS-2C Standard Committee, Architecture Analysis and Design Language (AADL)
Software Certification Consortium(SCC)
International Council on Systems Engineering (INCOSE), Northstar Chapter