John Franco

John V Franco

Professor

Rhodes Hall

831

CEAS - Elec Eng & Computer Science - 0030

Professional Summary

Prof. Franco is director of the National Center of Academic Excellence in Cyber Operations at the University of Cincinnati.  The Center is a collaborative effort involving three university colleges, and two local major defense contractors for advanced training in cyber operations and cyber security.

Prof. Franco is editor-in-chief of the Journal on Satisfiability, Boolean Modeling, and Computation, and an editor of the Annals of Mathematics and Artificial Intelligence.  He is Vice Chair of the SAT Association and a member of the steering committee for the annual Internation Conference on the Theory and Applications of Satisfiability Testing.

Prof. Franco has been PI, Co-PI, or Senior Personnel on 18 grants and contracts from the ONR, AFOSR, EPA, NSA, and NSF. He spent 9 months sabbatical leave at Fort George G. Meade in Research and Engineering on Satisfiability research, was visiting scientist at FAW, Ulm, Germany for three summers, and visiting scientist at U. Paderborn for a summer.
 

Education

Ph.D in Computer Science, Rutgers the State University of New Jersey 1981 (Computer Science)

M.S. in E.E., Columbia University New York, 1971 (Electrical Engineering)

B.S. in E.E., City College of New York New York City, 1969 (Electrical Engineering)

Research and Practice Interests

Information assurance, cyber defense, design & analysis of SAT algorithms, applications of SAT to network and computer security, formal methods, model checking, interactive first order logic theorem provers.

Research Support

Grant: #MDA90402C1162/P00005 Investigators:Franco, John 03-27-2002 -08-31-2004 National Security Agency Satisfiability Algorithm Research and Development to Enhance Formal Verification Tools Role:PI $561,906.00 Closed Level:Federal

Grant: #MDA90499C4547/P00004 Investigators:Franco, John 06-22-1999 -09-30-2001 National Security Agency Satisfiability Algorithm Research and Development to Enhance Formal Verification Tools Role:PI $493,185.00 Closed Level:Federal

Investigators:Franco, John 11-01-1998 -10-31-1999 Advanced Computing Systems Association Perl to JVM Optimization Role:PI $21,269.00 Closed Level:Private Non-Profit

Grant: #SRS 006291 Investigators:Franco, John 07-06-2009 -03-31-2010 National Security Agency Integrated Algebraic and Resolution Algorithms for Improved Solutions to Difficult Problems Role:PI $61,549.00 Closed Level:Federal

Grant: #DUE-1244697 Investigators:Bhattacharya, Prabir; Franco, John 09-15-2013 -08-31-2016 National Science Foundation Collaborative Research: Real World Relevant Security Labware for Mobile Analysis and Protection Experience Role:Collaborator $140,002.00 Awarded Level:Federal

Grant: #EEC-1404766 Investigators:Angelopoulos, Anastasios; Bhattacharya, Prabir; Cohen, Kelly; Franco, John; Guliants, Vadim; Kastner, Jeffrey; Kukreti, Anant; Kupferle, Margaret; Lu, Mingming; Nistor, Vasille; Sorial, George; Wei, Heng; Wendell, David 05-01-2014 -04-30-2017 National Science Foundation RET Site on "Challenge-Based Learning and Engineering Design Process Enhanced Research Experiences for Middle and High School In-Service Teachers." Role:Collaborator $498,949.00 Awarded Level:Federal

Grant: #0416-CS-PB-UC / NSF 1636995 Investigators:Franco, John 04-01-2016 -08-31-2017 National Science Foundation Real World Relevant Security Labware for Mobile Threat Analysis and Protection Experience Role:PI $21,300.00 Active Level:Federal

Grant: #H98230-17-1-0345 Investigators:Franco, John; Li, Chengcheng 07-01-2017 -06-30-2018 National Security Agency Train and Certify Qualified Instructors to Teach CAE's Cybersecurity Curricula Role:Collaborator $497,782.06 Awarded Level:Federal

Grant: #ODHE Cyber Range Investigators:Baker, Vicki; Cahay, Marc; Franco, John; Gerst, Jason; Harknett, Richard; Li, Chengcheng; Said, Hazem; Verkamp, Brian 07-01-2017 -06-30-2019 Ohio Department of Higher Education Ohio Cyber Range Role:Collaborator $1,900,000.00 Active Level:State of Ohio

Grant: #ODHE RAPIDS 2018 Investigators:Atluri, Gowtham; Franco, John; Li, Chengcheng 07-01-2017 -06-30-2018 Ohio Department of Higher Education RAPIDS Equipment Request Role:PI $253,395.00 Active Level:State of Ohio

Grant: #H98230-18-1-0333 Investigators:Franco, John 09-05-2018 -09-04-2019 National Security Agency 12.905 CAE-CO 2018/2019 Curriculum Development Initiatives Role:PI $59,999.97 Active Level:Federal

Grant: #H98230-19-1-0297 Investigators:Franco, John; Niu, Nan 09-01-2019 -08-31-2020 National Security Agency Automated detection and resolution of software vulnerabilities in critical and dependable systems where hundreds and thousands of features interact with each other in complex and subtle manners. Role:PI $92,193.00 Awarded Level:Federal

Publications

Peer Reviewed Publications

J Gu, PW Purdom, J Franco, BW Wah (1999. )Algorithms for the satisfiability (sat) problem .Handbook of Combinatorial Optimization, ,379 --572

J Franco, M Paull (1983. )Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem .Discrete Applied Mathematics, ,5 (1 ),77 --87

C Ming-Te, J Franco (1990. )Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem .Information Sciences , ,51 (4 ),289 --314

MT Chao, J Franco (1986. )Probabilistic analysis of two heuristics for the 3-satisfiability problem .SIAM Journal on Computing, ,15 (4 ),1106 --1118

J Franco, A Van Gelder (2003. )A perspective on certain polynomial-time solvable classes of satisfiability .Discrete Applied Mathematics, ,125 (2 ),177 --214

JS Schlipf, FS Annexstein, JV Franco, RP Swaminathan (1995. )On finding solutions for extended Horn formulas .Information Processing Letters, ,54 (3 ),133 --137

J. Franco (1986. )On the probabilistic performance of algorithms for the satisfiability problem .Information Processing Letters , ,23 (2 ),103 --106

J. Franco (2001. )Results related to threshold phenomena research in satisfiability: lower bounds .Theoretical Computer Science, ,265 (1 ),147 --157

DS Wise, J Franco (1990. )Costs of quadtree representation of nondense matrices .Journal of Parallel and Distributed Computing , ,9 (3 ),282 --296

J. Franco (1991. )Elimination of infrequent variables improves average case performance of satisfiability algorithms .SIAM Journal on Computing, ,20 (6 ),1119 --1127

J. Franco (1984. )Probabilistic analysis of the pure literal heuristic for the satisfiability problem .Annals of Operations Research, ,1 (3 ),273 --289

K Berman, J Schlipf, J Franco (1995. )Computing the well-founded semantics faster .Logic Programming and Nonmonotonic Reasoning, ,113 --126

J Franco, J Martin (2009. )A History of Satisfiability .Handbook of Satisfiability, ,185 ,3 --74

J Franco, M Kouril, J Schlipf, J Ward, S Weaver, M Dransfield, MW Vanfleet (2003. )SBSAT: a state-based, BDD-based satisfiability solver .International Conference on Theory and Applications of Satisfiability Testing , ,398 --410

J Franco, YC Ho (1988. )Probabilistic performance of a heuristic for the satisfiability problem .Discrete Applied Mathematics, ,22 (1 ),35 --51

V Franco, WM VanFleet, J Schlipf, MR Dransfield (2005. )Method and system for non-linear state based satisfiability .US Patent 6,912,700, ,

M Kouril, J Franco (2005. )Resolution tunnels for improved SAT solver performance .International Conference on Theory and Applications of Satisfiability Testing, ,143 --157

LC Murdoch, J Franco (1994. )The analysis of constant drawdown wells using instantaneous source functions .Water resources research, ,30 (1 ),117 --124

J Franco, J Goldsmith, J Schlipf, E Speckenmeyer, RP Swaminathan (1999. )An algorithm for the class of pure implicational formulas .Discrete Applied Mathematics, ,96 ,89 --106

MN Velev, J Franco (2014. )Application of constraints to formal verification and artificial intelligence .Ann. Math. Artif. Intell. , ,70 (4 ),313 --314

W Yue, J Franco, Q Han, W Cao (2014. )Improved anytime d* algorithm .IAENG Transactions on Engineering Technologies, ,383 --396

J Franco, S Weaver (2013. )Algorithms for the Satisfiability Problem .Handbook of Combinatorial Optimization, ,311 --454

Franco J.; Velev M. (01-01-2014. )Application of constraints to formal verification and artificial intelligence.Annals of Mathematics and Artificial Intelligence, ,70 (4 ),313-314

Cao W.; Franco J.; Han Q.; Yue W. (01-01-2014. )Improved anytime D*algorithm.Lecture Notes in Electrical Engineering, ,247 LNEE ,383-396

Franco J.; Weaver S. (01-01-2013. )Algorithms for the satisfiability problem.Handbook of Combinatorial Optimization, ,1-5 ,311-454

Cao W.; Franco J.; Han Q.; Yue W. (01-01-2012. )A new anytime dynamic navigation algorithm .Lecture Notes in Engineering and Computer Science, ,1 ,17-22

Cao W.; Franco J.; Yue H.; Yue W. (06-23-2011. )ID*Lite: Improved D*Lite algorithm.Proceedings of the ACM Symposium on Applied Computing, ,1364-1369

Franco J. (03-01-2011. )Preface to the special issue.Annals of Mathematics and Artificial Intelligence, ,61 (3 ),155-157

Franco J.; Yue W. (11-23-2010. )A new way to reduce computing in navigation algorithm .Engineering Letters, ,18 (4 ),

Franco J.; Martin J. (01-01-2009. )A history of satisfiability.Frontiers in Artificial Intelligence and Applications, ,185 (1 ),3-74

Franco J. (12-01-2005. )Typical case complexity of Satisfiability algorithms and the threshold phenomenon.Discrete Applied Mathematics, ,153 (1-3 ),89-123

Creignou N.; Daudé H.; Franco J. (12-01-2005. )A sharp threshold for the renameable-Horn and the q-Horn properties.Discrete Applied Mathematics, ,153 (1-3 ),48-57

Franco J.; Kouril M. (10-17-2005. )Resolution tunnels for improved SAT solver performance .Lecture Notes in Computer Science, ,3569 ,143-157

Dransfield M.; Franco J.; Kouril M.; Schlipf J.; Vanfleet W.; Weaver S. (12-01-2004. )Function-complete lookahead in support of efficient SAT search heuristics .Journal of Universal Computer Science, ,10 (12 ),1655-1692

Dransfield M.; Franco J.; Kouril M.; Mark Vanfleet W.; Schlipf J.; Ward J.; Weaver S. (12-01-2004. )SBSAT: A state-based, BDD-based satisfiability solver .Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ,2919 ,398-410

Franco J.; Swaminathan R. (08-15-2003. )On good algorithms for determining unsatisfiability of propositional formulas.Discrete Applied Mathematics, ,130 (2 ),129-138

Franco J.; Van Gelder A. (02-01-2003. )A perspective on certain polynomial-time solvable classes of satisfiability.Discrete Applied Mathematics, ,125 (2-3 ),177-214

Franco J. (09-03-2001. )Results related to threshold phenomena research in satisfiability: Lower bounds.Theoretical Computer Science, ,265 (1-2 ),147-157

Franco J. (12-01-2000. )Some interesting research directions in satisfiability .Annals of Mathematics and Artificial Intelligence, ,28 (1-4 ),7-15

Franco J.; Goldsmith J.; Schlipf J.; Speckenmeyer E.; Swaminathan R. (10-15-1999. )An algorithm for the class of pure implicational formulas.Discrete Applied Mathematics, ,96-97 ,89-106

Franco J.; Plotkin J.; Rosenthal J. (01-01-1999. )Probability of pure literals.Journal of Logic and Computation, ,9 (4 ),501-513

Franco J.; Swaminathan R. (12-01-1997. )Average case results for satisfiability algorithms under the random-clause-width model .Annals of Mathematics and Artificial Intelligence, ,20 (1-4 ),357-391

Annexstein F.; Franco J. (06-23-1995. )Work-preserving emulations of shuffle-exchange networks: An analysis of the complex plane diagram.Discrete Applied Mathematics, ,60 (1-3 ),13-23

Berman K.; Franco J.; Schlipf J. (06-23-1995. )Unique satisfiability of Horn sets can be solved in nearly linear time.Discrete Applied Mathematics, ,60 (1-3 ),77-91

Annexstein F.; Franco J.; Schlipf J.; Swaminathan R. (05-12-1995. )On finding solutions for extended Horn formulas.Information Processing Letters, ,54 (3 ),133-137

Berman K.; Franco J.; Schlipf J. (01-01-1995. )Computing the well-founded semantics faster .Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ,928 ,113-126

Franco J. (02-09-1993. )On the occurrence of null clauses in random instances of satisfiability.Discrete Applied Mathematics, ,41 (3 ),203-209

Dunn J.; Franco J.; Wheeler W. (03-01-1992. )Recent work at the interface of logic, combinatorics, and computer science.Annals of Mathematics and Artificial Intelligence, ,6 (1-3 ),1-15

Celis P.; Franco J. (01-01-1992. )The analysis of hashing with lazy deletions.Information Sciences, ,62 (1-2 ),13-26

Franco J. (01-01-1991. )Elimination of infrequent variables improves average case performance of satisfiability algorithms.SIAM Journal on Computing, ,20 (6 ),1119-1127

Franco J.; Friedman D. (01-01-1990. )Towards a facility for lexically scoped, dynamic mutual recursion in Scheme.Computer Languages, ,15 (1 ),55-64

Franco J.; Ming-Te C. (01-01-1990. )Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k.Information Sciences, ,51 (3 ),289-314

Franco J.; Wise D. (01-01-1990. )Costs of quadtree representation of nondense matrices.Journal of Parallel and Distributed Computing, ,9 (3 ),282-296

Franco J.; Friedman D.; Johnson S. (01-01-1990. )Multi-way streams in Scheme.Computer Languages, ,15 (2 ),109-125

Franco J.; Friedman D. (01-01-1989. )Creating efficient programs by exchanging data for procedures.Computer Languages, ,14 (1 ),11-23

Franco J.; Ho Y. (01-01-1988. )Probabilistic performance of a heuristic for the satisfiability problem.Discrete Applied Mathematics, ,22 (1 ),35-51

Franco J.; Plotkin J.; Rosenthal J. (01-01-1987. )Correction to probabilistic analysis of the Davis Putnam procedure for solving the satisfiability pr.Discrete Applied Mathematics, ,17 (3 ),295-299

Franco J. (08-20-1986. )On the probabilistic performance of algorithms for the satisfiability problem.Information Processing Letters, ,23 (2 ),103-106

Choukhmane E.; Franco J. (01-01-1986. )An approximation algorithm for the maximum independent set problem in cubic planar graphs.Networks, ,16 (4 ),349-356

Chao M.; Franco J. (01-01-1986. )PROBABILISTIC ANALYSIS OF TWO HEURISTICS FOR THE 3-SATISFIABILITY PROBLEM.SIAM Journal on Computing, ,15 (4 ),1106-1118

Franco J. (10-01-1984. )Probabilistic analysis of the pure literal heuristic for the satisfiability problem.Annals of Operations Research, ,1 (3 ),273-289

Franco J.; Paull M. (01-01-1983. )Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem.Discrete Applied Mathematics, ,5 (1 ),77-87

Book Chapter

J Franco and S. Weaver (2013 )Algorithms for the Satisfiability Problem Handbook on Combinatorial Optimization .(pp. 311--454).Springer(Author)

J. Franco (2010 )Probabilistic analysis of Satisfiability algorithms Boolean Methods and Models .

J. Franco and J. Martin (2009 )A History of Satisfiability Handbook on Satisfiability .IOS Press

J. Gu, P.W. Purdom, J. Franco, and B.W. Wah (2002 )Algorithms for the Satisfiability (SAT) Problem Handbook of Applied Optimization .(pp. 640--660).Oxford University Press

J. Gu, P.W. Purdom, J. Franco, and B. Wah (1999 )Algorithms for the Satisfiability (SAT) Problem Handbook of Combinatorial Optimization, Supplement Volume A .Kluwer