John V Franco

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.
 

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)

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.

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

Grant: #Riverside Research Institute DRC.11373.RR001834.20 sub WSARC sub OFRN Investigators:Franco, John 03-01-2020 -08-31-2021 Wright State Applied Research Corporation Computer-Human Interaction for Rapid Program Analysis through Cognitive Collaboration (CHIRP2C) Role:PI $100,000.00 Awarded Level:Private Non-Profit

Grant: #H98230-20-1-0365 Investigators:Franco, John; Niu, Nan 09-10-2020 -12-30-2021 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 $72,392.00 Awarded Level:Federal

Grant: #H98230-21-1-0315 Investigators:Franco, John; Niu, Nan 08-23-2021 -12-31-2022 National Security Agency Automated Reverse Engineering Tools and Detection and Resolution of Software vulnerabilities in Critical and Dependable Systems Role:PI 72431.00 Awarded Level:Federal

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 More Information

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

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

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

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

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

Yue W.;Franco J. (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 More Information

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

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 More Information

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

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

Franco J.;Kouril M.;Schlipf J.;Ward J.;Weaver S.;Dransfield M.;Mark Vanfleet W. (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 More Information

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 More Information

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

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 More Information

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

Franco J.;Swaminathan R.P. (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 More Information

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 More Information

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

Berman K.A.;Schlipf J.S.;Franco J.V. (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 More Information

Franco J.;Dunn 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 More Information

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

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

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

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

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

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

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

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

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 More Information

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

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 More Information

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 More Information

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

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 More Information

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

https://scholar.google.com/citations?user=ldgiV80AAAAJ&hl=en&oi=ao,

Google Scholar Profile